10725#line 1427
10726 tmp___1 = __VERIFIER_nondet_int();
10727 }
10728#line 1427
10729 if (tmp___1 != 0) {
10730#line 1428
10731 goto ldv_22508;
10732 } else {
10733#line 1430
10734 goto ldv_22510;
10735 }
10736 ldv_22510: ;
10737 {
10738#line 1735
10739 cleanup_ftl();
10740 }
10741 ldv_final:
10742 {
10743#line 1738
10744 ldv_check_final_state();
10745 }
10746#line 1741
10747 return;
10748}
10749}
10750#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11861/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
10751void ldv_blast_assert(void)
10752{
10753
10754 {
10755 ERROR: ;
10756#line 6
10757 goto ERROR;
10758}
10759}
10760#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11861/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
10761extern int __VERIFIER_nondet_int(void) ;
10762#line 1762 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11861/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/ftl.c.p"
10763int ldv_spin = 0;
10764#line 1766 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11861/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/ftl.c.p"
10765void ldv_check_alloc_flags(gfp_t flags )