3845 goto ldv_24983;
3846 } else
3847#line 314
3848 if (ldv_s_sedlbauer_driver_pcmcia_driver != 0) {
3849#line 316
3850 goto ldv_24983;
3851 } else {
3852#line 318
3853 goto ldv_24985;
3854 }
3855 ldv_24985: ;
3856 ldv_module_exit:
3857 {
3858#line 383
3859 exit_sedlbauer_cs();
3860 }
3861 ldv_final:
3862 {
3863#line 386
3864 ldv_check_final_state();
3865 }
3866#line 389
3867 return;
3868}
3869}
3870#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4087/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3871void ldv_blast_assert(void)
3872{
3873
3874 {
3875 ERROR: ;
3876#line 6
3877 goto ERROR;
3878}
3879}
3880#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4087/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3881extern int __VERIFIER_nondet_int(void) ;
3882#line 410 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4087/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hisax/sedlbauer_cs.c.p"
3883int ldv_spin = 0;
3884#line 414 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4087/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hisax/sedlbauer_cs.c.p"
3885void ldv_check_alloc_flags(gfp_t flags )