6216#line 820
6217 tmp___1 = __VERIFIER_nondet_int();
6218 }
6219#line 820
6220 if (tmp___1 != 0) {
6221#line 821
6222 goto ldv_18826;
6223 } else {
6224#line 823
6225 goto ldv_18828;
6226 }
6227 ldv_18828: ;
6228 {
6229#line 839
6230 mtd_oobtest_exit();
6231 }
6232 ldv_final:
6233 {
6234#line 842
6235 ldv_check_final_state();
6236 }
6237#line 845
6238 return;
6239}
6240}
6241#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11603/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6242void ldv_blast_assert(void)
6243{
6244
6245 {
6246 ERROR: ;
6247#line 6
6248 goto ERROR;
6249}
6250}
6251#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11603/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6252extern int __VERIFIER_nondet_int(void) ;
6253#line 866 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11603/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/tests/mtd_oobtest.c.p"
6254int ldv_spin = 0;
6255#line 870 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11603/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/tests/mtd_oobtest.c.p"
6256void ldv_check_alloc_flags(gfp_t flags )