16809 }
16810 }
16811 }
16812 {
16813#line 1594
16814 __cil_tmp68 = b->bm_set;
16815#line 1594
16816 weight = __cil_tmp68 - weight;
16817#line 1595
16818 __cil_tmp69 = & b->bm_lock;
16819#line 1595
16820 spin_unlock_irq(__cil_tmp69);
16821 }
16822#line 1596
16823 return (weight);
16824}
16825}
16826#line 1615
16827void ldv_check_final_state(void) ;
16828#line 1621
16829extern void ldv_initialize(void) ;
16830#line 1624
16831extern int nondet_int(void) ;
16832#line 1627 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/drbd/drbd.ko--X--unsafe1_safe6linux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/19/dscv_tempdir/dscv/ri/08_1/drivers/block/drbd/drbd_bitmap.c.p"
16833int LDV_IN_INTERRUPT ;
16834#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/drbd/drbd.ko--X--unsafe1_safe6linux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/19/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
16835void ldv_blast_assert(void)
16836{
16837
16838 {
16839 ERROR: ;
16840#line 6
16841 goto ERROR;
16842}
16843}
16844#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/drbd/drbd.ko--X--unsafe1_safe6linux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/19/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
16845extern int ldv_undefined_int(void) ;
16846#line 1687 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/drbd/drbd.ko--X--unsafe1_safe6linux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/19/dscv_tempdir/dscv/ri/08_1/drivers/block/drbd/drbd_bitmap.c.p"
16847int ldv_module_refcounter = 1;
16848#line 1690 "/anthill/stuff/tacas-comp/work/current--X--drivers/block/drbd/drbd.ko--X--unsafe1_safe6linux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/19/dscv_tempdir/dscv/ri/08_1/drivers/block/drbd/drbd_bitmap.c.p"
16849void ldv_module_get(struct module *module )