8501#line 1114
8502 tmp___1 = __VERIFIER_nondet_int();
8503 }
8504#line 1114
8505 if (tmp___1 != 0) {
8506#line 1115
8507 goto ldv_19818;
8508 } else {
8509#line 1117
8510 goto ldv_19820;
8511 }
8512 ldv_19820: ;
8513 {
8514#line 1249
8515 cleanup_inftl();
8516 }
8517 ldv_final:
8518 {
8519#line 1252
8520 ldv_check_final_state();
8521 }
8522#line 1255
8523 return;
8524}
8525}
8526#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11741/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
8527void ldv_blast_assert(void)
8528{
8529
8530 {
8531 ERROR: ;
8532#line 6
8533 goto ERROR;
8534}
8535}
8536#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11741/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
8537extern int __VERIFIER_nondet_int(void) ;
8538#line 1276 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11741/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/inftlcore.c.p"
8539int ldv_spin = 0;
8540#line 1280 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11741/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/inftlcore.c.p"
8541void ldv_check_alloc_flags(gfp_t flags )