5506 tmp___0 = __VERIFIER_nondet_int();
5507 }
5508#line 602
5509 if (tmp___0 != 0) {
5510#line 604
5511 goto ldv_21398;
5512 } else
5513#line 602
5514 if (ldv_s_rtc_device_driver_platform_driver != 0) {
5515#line 604
5516 goto ldv_21398;
5517 } else {
5518#line 606
5519 goto ldv_21400;
5520 }
5521 ldv_21400: ;
5522 ldv_module_exit: ;
5523 {
5524#line 884
5525 ldv_check_final_state();
5526 }
5527#line 887
5528 return;
5529}
5530}
5531#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5532void ldv_blast_assert(void)
5533{
5534
5535 {
5536 ERROR: ;
5537#line 6
5538 goto ERROR;
5539}
5540}
5541#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5542extern int __VERIFIER_nondet_int(void) ;
5543#line 908 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5544int ldv_spin = 0;
5545#line 912 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5546void ldv_check_alloc_flags(gfp_t flags )