4177 }
4178 ldv_23851: ;
4179 ldv_23855:
4180 {
4181#line 307
4182 tmp___0 = __VERIFIER_nondet_int();
4183 }
4184#line 307
4185 if (tmp___0 != 0) {
4186#line 308
4187 goto ldv_23854;
4188 } else {
4189#line 310
4190 goto ldv_23856;
4191 }
4192 ldv_23856: ;
4193
4194 {
4195#line 365
4196 ldv_check_final_state();
4197 }
4198#line 368
4199 return;
4200}
4201}
4202#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2640/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4203void ldv_blast_assert(void)
4204{
4205
4206 {
4207 ERROR: ;
4208#line 6
4209 goto ERROR;
4210}
4211}
4212#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2640/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4213extern int __VERIFIER_nondet_int(void) ;
4214#line 389 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2640/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-ds1672.c.p"
4215int ldv_spin = 0;
4216#line 393 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2640/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-ds1672.c.p"
4217void ldv_check_alloc_flags(gfp_t flags )