7402 goto ldv_40330;
7403 } else
7404#line 422
7405 if (ldv_s_orinoco_nortel_driver_pci_driver != 0) {
7406#line 424
7407 goto ldv_40330;
7408 } else {
7409#line 426
7410 goto ldv_40332;
7411 }
7412 ldv_40332: ;
7413 ldv_module_exit:
7414 {
7415#line 469
7416 orinoco_nortel_exit();
7417 }
7418 ldv_final:
7419 {
7420#line 472
7421 ldv_check_final_state();
7422 }
7423#line 475
7424 return;
7425}
7426}
7427#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13879/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7428void ldv_blast_assert(void)
7429{
7430
7431 {
7432 ERROR: ;
7433#line 6
7434 goto ERROR;
7435}
7436}
7437#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13879/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7438extern int __VERIFIER_nondet_int(void) ;
7439#line 496 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13879/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/orinoco/orinoco_nortel.c.p"
7440int ldv_spin = 0;
7441#line 500 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13879/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/orinoco/orinoco_nortel.c.p"
7442void ldv_check_alloc_flags(gfp_t flags )