6929 goto ldv_40316;
6930 } else
6931#line 371
6932 if (ldv_s_orinoco_pci_driver_pci_driver != 0) {
6933#line 373
6934 goto ldv_40316;
6935 } else {
6936#line 375
6937 goto ldv_40318;
6938 }
6939 ldv_40318: ;
6940 ldv_module_exit:
6941 {
6942#line 424
6943 orinoco_pci_exit();
6944 }
6945 ldv_final:
6946 {
6947#line 427
6948 ldv_check_final_state();
6949 }
6950#line 430
6951 return;
6952}
6953}
6954#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13880/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6955void ldv_blast_assert(void)
6956{
6957
6958 {
6959 ERROR: ;
6960#line 6
6961 goto ERROR;
6962}
6963}
6964#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13880/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6965extern int __VERIFIER_nondet_int(void) ;
6966#line 451 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13880/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/orinoco/orinoco_pci.c.p"
6967int ldv_spin = 0;
6968#line 455 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13880/dscv_tempdir/dscv/ri/43_1a/drivers/net/wireless/orinoco/orinoco_pci.c.p"
6969void ldv_check_alloc_flags(gfp_t flags )