3869 tmp___0 = __VERIFIER_nondet_int();
3870 }
3871#line 1039
3872 if (tmp___0 != 0) {
3873#line 1041
3874 goto ldv_21309;
3875 } else
3876#line 1039
3877 if (ldv_s_wm831x_rtc_driver_platform_driver != 0) {
3878#line 1041
3879 goto ldv_21309;
3880 } else {
3881#line 1043
3882 goto ldv_21311;
3883 }
3884 ldv_21311: ;
3885 ldv_module_exit: ;
3886 {
3887#line 1655
3888 ldv_check_final_state();
3889 }
3890#line 1658
3891 return;
3892}
3893}
3894#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3895void ldv_blast_assert(void)
3896{
3897
3898 {
3899 ERROR: ;
3900#line 6
3901 goto ERROR;
3902}
3903}
3904#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3905extern int __VERIFIER_nondet_int(void) ;
3906#line 1679 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3907int ldv_spin = 0;
3908#line 1683 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3909void ldv_check_alloc_flags(gfp_t flags )