4045 goto ldv_24988;
4046 } else
4047#line 305
4048 if (ldv_s_teles_cs_driver_pcmcia_driver != 0) {
4049#line 307
4050 goto ldv_24988;
4051 } else {
4052#line 309
4053 goto ldv_24990;
4054 }
4055 ldv_24990: ;
4056 ldv_module_exit:
4057 {
4058#line 374
4059 exit_teles_cs();
4060 }
4061 ldv_final:
4062 {
4063#line 377
4064 ldv_check_final_state();
4065 }
4066#line 380
4067 return;
4068}
4069}
4070#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4088/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4071void ldv_blast_assert(void)
4072{
4073
4074 {
4075 ERROR: ;
4076#line 6
4077 goto ERROR;
4078}
4079}
4080#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4088/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4081extern int __VERIFIER_nondet_int(void) ;
4082#line 401 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4088/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hisax/teles_cs.c.p"
4083int ldv_spin = 0;
4084#line 405 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4088/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hisax/teles_cs.c.p"
4085void ldv_check_alloc_flags(gfp_t flags )