15148#line 901
15149 tmp___1 = __VERIFIER_nondet_int();
15150 }
15151#line 901
15152 if (tmp___1 != 0) {
15153#line 902
15154 goto ldv_41318;
15155 } else {
15156#line 904
15157 goto ldv_41320;
15158 }
15159 ldv_41320: ;
15160 {
15161#line 950
15162 budget_exit();
15163 }
15164 ldv_final:
15165 {
15166#line 953
15167 ldv_check_final_state();
15168 }
15169#line 956
15170 return;
15171}
15172}
15173#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8262/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
15174void ldv_blast_assert(void)
15175{
15176
15177 {
15178 ERROR: ;
15179#line 6
15180 goto ERROR;
15181}
15182}
15183#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8262/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
15184extern int __VERIFIER_nondet_int(void) ;
15185#line 977 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8262/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/ttpci/budget.c.p"
15186int ldv_spin = 0;
15187#line 981 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8262/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/ttpci/budget.c.p"
15188void ldv_check_alloc_flags(gfp_t flags )