9527 tmp___0 = __VERIFIER_nondet_int();
9528 }
9529#line 669
9530 if (tmp___0 != 0) {
9531#line 671
9532 goto ldv_39114;
9533 } else
9534#line 669
9535 if (ldv_s_dibusb_driver_usb_driver != 0) {
9536#line 671
9537 goto ldv_39114;
9538 } else {
9539#line 673
9540 goto ldv_39116;
9541 }
9542 ldv_39116: ;
9543 ldv_module_exit: ;
9544 {
9545#line 912
9546 ldv_check_final_state();
9547 }
9548#line 915
9549 return;
9550}
9551}
9552#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8573/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
9553void ldv_blast_assert(void)
9554{
9555
9556 {
9557 ERROR: ;
9558#line 6
9559 goto ERROR;
9560}
9561}
9562#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8573/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
9563extern int __VERIFIER_nondet_int(void) ;
9564#line 936 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8573/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/dvb-usb/dibusb-mb.c.p"
9565int ldv_spin = 0;
9566#line 940 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8573/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/dvb-usb/dibusb-mb.c.p"
9567void ldv_check_alloc_flags(gfp_t flags )