11974#line 814
11975 tmp___1 = __VERIFIER_nondet_int();
11976 }
11977#line 814
11978 if (tmp___1 != 0) {
11979#line 815
11980 goto ldv_42878;
11981 } else {
11982#line 817
11983 goto ldv_42880;
11984 }
11985 ldv_42880: ;
11986 {
11987#line 907
11988 budget_patch_exit();
11989 }
11990 ldv_final:
11991 {
11992#line 910
11993 ldv_check_final_state();
11994 }
11995#line 913
11996 return;
11997}
11998}
11999#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8261/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
12000void ldv_blast_assert(void)
12001{
12002
12003 {
12004 ERROR: ;
12005#line 6
12006 goto ERROR;
12007}
12008}
12009#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8261/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
12010extern int __VERIFIER_nondet_int(void) ;
12011#line 934 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8261/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/ttpci/budget-patch.c.p"
12012int ldv_spin = 0;
12013#line 938 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8261/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/ttpci/budget-patch.c.p"
12014void ldv_check_alloc_flags(gfp_t flags )