5381 goto ldv_35162;
5382 } else
5383#line 211
5384 if (ldv_s_idepnp_driver_pnp_driver != 0) {
5385#line 213
5386 goto ldv_35162;
5387 } else {
5388#line 215
5389 goto ldv_35164;
5390 }
5391 ldv_35164: ;
5392 ldv_module_exit:
5393 {
5394#line 270
5395 pnpide_exit();
5396 }
5397 ldv_final:
5398 {
5399#line 273
5400 ldv_check_final_state();
5401 }
5402#line 276
5403 return;
5404}
5405}
5406#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1158/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5407void ldv_blast_assert(void)
5408{
5409
5410 {
5411 ERROR: ;
5412#line 6
5413 goto ERROR;
5414}
5415}
5416#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1158/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5417extern int __VERIFIER_nondet_int(void) ;
5418#line 297 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1158/dscv_tempdir/dscv/ri/43_1a/drivers/ide/ide-pnp.c.p"
5419int ldv_spin = 0;
5420#line 301 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1158/dscv_tempdir/dscv/ri/43_1a/drivers/ide/ide-pnp.c.p"
5421void ldv_check_alloc_flags(gfp_t flags )