9082#line 967
9083 tmp___1 = __VERIFIER_nondet_int();
9084 }
9085#line 967
9086 if (tmp___1 != 0) {
9087#line 968
9088 goto ldv_28430;
9089 } else {
9090#line 970
9091 goto ldv_28432;
9092 }
9093 ldv_28432: ;
9094 {
9095#line 1016
9096 zram_exit();
9097 }
9098 ldv_final:
9099 {
9100#line 1019
9101 ldv_check_final_state();
9102 }
9103#line 1022
9104 return;
9105}
9106}
9107#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5798/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
9108void ldv_blast_assert(void)
9109{
9110
9111 {
9112 ERROR: ;
9113#line 6
9114 goto ERROR;
9115}
9116}
9117#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5798/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
9118extern int __VERIFIER_nondet_int(void) ;
9119#line 1043 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5798/dscv_tempdir/dscv/ri/43_1a/drivers/staging/zram/zram_drv.c.p"
9120int ldv_spin = 0;
9121#line 1047 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5798/dscv_tempdir/dscv/ri/43_1a/drivers/staging/zram/zram_drv.c.p"
9122void ldv_check_alloc_flags(gfp_t flags )