4374#line 613
4375 tmp___1 = __VERIFIER_nondet_int();
4376 }
4377#line 613
4378 if (tmp___1 != 0) {
4379#line 614
4380 goto ldv_21145;
4381 } else {
4382#line 616
4383 goto ldv_21147;
4384 }
4385 ldv_21147: ;
4386 {
4387#line 812
4388 mc13xxx_rtc_exit();
4389 }
4390 ldv_final:
4391 {
4392#line 815
4393 ldv_check_final_state();
4394 }
4395#line 818
4396 return;
4397}
4398}
4399#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4400void ldv_blast_assert(void)
4401{
4402
4403 {
4404 ERROR: ;
4405#line 6
4406 goto ERROR;
4407}
4408}
4409#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4410extern int __VERIFIER_nondet_int(void) ;
4411#line 839 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4412int ldv_spin = 0;
4413#line 843 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4414void ldv_check_alloc_flags(gfp_t flags )