5871#line 568
5872 tmp___1 = __VERIFIER_nondet_int();
5873 }
5874#line 568
5875 if (tmp___1 != 0) {
5876#line 569
5877 goto ldv_20495;
5878 } else {
5879#line 571
5880 goto ldv_20497;
5881 }
5882 ldv_20497: ;
5883 {
5884#line 629
5885 mtdoops_exit();
5886 }
5887 ldv_final:
5888 {
5889#line 632
5890 ldv_check_final_state();
5891 }
5892#line 635
5893 return;
5894}
5895}
5896#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5897void ldv_blast_assert(void)
5898{
5899
5900 {
5901 ERROR: ;
5902#line 6
5903 goto ERROR;
5904}
5905}
5906#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5907extern int __VERIFIER_nondet_int(void) ;
5908#line 656 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5909int ldv_spin = 0;
5910#line 660 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11887/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/mtdoops.c.p"
5911void ldv_check_alloc_flags(gfp_t flags )