7314 goto ldv_40334;
7315 } else
7316#line 478
7317 if (ldv_s_orinoco_plx_driver_pci_driver != 0) {
7318#line 480
7319 goto ldv_40334;
7320 } else {
7321#line 482
7322 goto ldv_40336;
7323 }
7324 ldv_40336: ;
7325 ldv_module_exit:
7326 {
7327#line 533
7328 orinoco_plx_exit();
7329 }
7330 ldv_final:
7331 {
7332#line 536
7333 ldv_check_final_state();
7334 }
7335#line 539
7336 return;
7337}
7338}
7339#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13881/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7340void ldv_blast_assert(void)
7341{
7342
7343 {
7344 ERROR: ;
7345#line 6
7346 goto ERROR;
7347}
7348}
7349#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13881/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7350extern int __VERIFIER_nondet_int(void) ;
7351#line 560 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13881/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/orinoco/orinoco_plx.c.p"
7352int ldv_spin = 0;
7353#line 564 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13881/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/orinoco/orinoco_plx.c.p"
7354void ldv_check_alloc_flags(gfp_t flags )