12672 goto ldv_39223;
12673 } else
12674#line 1229
12675 if (ldv_s_az6007_usb_driver_usb_driver != 0) {
12676#line 1231
12677 goto ldv_39223;
12678 } else {
12679#line 1233
12680 goto ldv_39225;
12681 }
12682 ldv_39225: ;
12683 ldv_module_exit:
12684 {
12685#line 1534
12686 az6007_usb_module_exit();
12687 }
12688 ldv_final:
12689 {
12690#line 1537
12691 ldv_check_final_state();
12692 }
12693#line 1540
12694 return;
12695}
12696}
12697#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8596/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
12698void ldv_blast_assert(void)
12699{
12700
12701 {
12702 ERROR: ;
12703#line 6
12704 goto ERROR;
12705}
12706}
12707#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8596/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
12708extern int __VERIFIER_nondet_int(void) ;
12709#line 1561 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8596/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/dvb-usb/az6007.c.p"
12710int ldv_spin = 0;
12711#line 1565 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8596/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/dvb-usb/az6007.c.p"
12712void ldv_check_alloc_flags(gfp_t flags )