12006 tmp___0 = __VERIFIER_nondet_int();
12007 }
12008#line 1111
12009 if (tmp___0 != 0) {
12010#line 1113
12011 goto ldv_39243;
12012 } else
12013#line 1111
12014 if (ldv_s_ttusb2_driver_usb_driver != 0) {
12015#line 1113
12016 goto ldv_39243;
12017 } else {
12018#line 1115
12019 goto ldv_39245;
12020 }
12021 ldv_39245: ;
12022 ldv_module_exit: ;
12023 {
12024#line 1531
12025 ldv_check_final_state();
12026 }
12027#line 1534
12028 return;
12029}
12030}
12031#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8582/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
12032void ldv_blast_assert(void)
12033{
12034
12035 {
12036 ERROR: ;
12037#line 6
12038 goto ERROR;
12039}
12040}
12041#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8582/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
12042extern int __VERIFIER_nondet_int(void) ;
12043#line 1555 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8582/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/dvb-usb/ttusb2.c.p"
12044int ldv_spin = 0;
12045#line 1559 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8582/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/dvb-usb/ttusb2.c.p"
12046void ldv_check_alloc_flags(gfp_t flags )