16402 tmp___0 = __VERIFIER_nondet_int();
16403 }
16404#line 3356
16405 if (tmp___0 != 0) {
16406#line 3358
16407 goto ldv_40785;
16408 } else
16409#line 3356
16410 if (ldv_s_orinoco_driver_usb_driver != 0) {
16411#line 3358
16412 goto ldv_40785;
16413 } else {
16414#line 3360
16415 goto ldv_40787;
16416 }
16417 ldv_40787: ;
16418 ldv_module_exit: ;
16419 {
16420#line 5052
16421 ldv_check_final_state();
16422 }
16423#line 5055
16424 return;
16425}
16426}
16427#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13883/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
16428void ldv_blast_assert(void)
16429{
16430
16431 {
16432 ERROR: ;
16433#line 6
16434 goto ERROR;
16435}
16436}
16437#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13883/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
16438extern int __VERIFIER_nondet_int(void) ;
16439#line 5076 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13883/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/orinoco/orinoco_usb.c.p"
16440int ldv_spin = 0;
16441#line 5080 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13883/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/orinoco/orinoco_usb.c.p"
16442void ldv_check_alloc_flags(gfp_t flags )