4426#line 557
4427 tmp___1 = __VERIFIER_nondet_int();
4428 }
4429#line 557
4430 if (tmp___1 != 0) {
4431#line 558
4432 goto ldv_28296;
4433 } else {
4434#line 560
4435 goto ldv_28298;
4436 }
4437 ldv_28298: ;
4438 {
4439#line 590
4440 block2mtd_exit();
4441 }
4442 ldv_final:
4443 {
4444#line 593
4445 ldv_check_final_state();
4446 }
4447#line 596
4448 return;
4449}
4450}
4451#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11710/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4452void ldv_blast_assert(void)
4453{
4454
4455 {
4456 ERROR: ;
4457#line 6
4458 goto ERROR;
4459}
4460}
4461#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11710/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4462extern int __VERIFIER_nondet_int(void) ;
4463#line 617 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11710/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/block2mtd.c.p"
4464int ldv_spin = 0;
4465#line 621 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11710/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/block2mtd.c.p"
4466void ldv_check_alloc_flags(gfp_t flags )