7775 {
7776#line 1159
7777 tmp___0 = __VERIFIER_nondet_int();
7778 }
7779#line 1159
7780 if (tmp___0 != 0) {
7781#line 1160
7782 goto ldv_19542;
7783 } else {
7784#line 1162
7785 goto ldv_19544;
7786 }
7787 ldv_19544: ;
7788 {
7789#line 1197
7790 cleanup_doc2001plus();
7791 }
7792 {
7793#line 1200
7794 ldv_check_final_state();
7795 }
7796#line 1203
7797 return;
7798}
7799}
7800#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11713/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7801void ldv_blast_assert(void)
7802{
7803
7804 {
7805 ERROR: ;
7806#line 6
7807 goto ERROR;
7808}
7809}
7810#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11713/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7811extern int __VERIFIER_nondet_int(void) ;
7812#line 1224 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11713/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/doc2001plus.c.p"
7813int ldv_spin = 0;
7814#line 1228 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11713/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/doc2001plus.c.p"
7815void ldv_check_alloc_flags(gfp_t flags )