2402#line 302
2403 tmp___1 = __VERIFIER_nondet_int();
2404 }
2405#line 302
2406 if (tmp___1 != 0) {
2407#line 303
2408 goto ldv_23190;
2409 } else {
2410#line 305
2411 goto ldv_23192;
2412 }
2413 ldv_23192: ;
2414 {
2415#line 319
2416 b1pcmcia_exit();
2417 }
2418 ldv_final:
2419 {
2420#line 322
2421 ldv_check_final_state();
2422 }
2423#line 325
2424 return;
2425}
2426}
2427#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2428void ldv_blast_assert(void)
2429{
2430
2431 {
2432 ERROR: ;
2433#line 6
2434 goto ERROR;
2435}
2436}
2437#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2438extern int __VERIFIER_nondet_int(void) ;
2439#line 346 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2440int ldv_spin = 0;
2441#line 350 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4160/dscv_tempdir/dscv/ri/43_1a/drivers/isdn/hardware/avm/b1pcmcia.c.p"
2442void ldv_check_alloc_flags(gfp_t flags )