2175 tmp___0 = __VERIFIER_nondet_int();
2176 }
2177#line 315
2178 if (tmp___0 != 0) {
2179#line 317
2180 goto ldv_17581;
2181 } else
2182#line 315
2183 if (ldv_s_wm831x_backup_driver_platform_driver != 0) {
2184#line 317
2185 goto ldv_17581;
2186 } else {
2187#line 319
2188 goto ldv_17583;
2189 }
2190 ldv_17583: ;
2191 ldv_module_exit: ;
2192 {
2193#line 349
2194 ldv_check_final_state();
2195 }
2196#line 352
2197 return;
2198}
2199}
2200#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2201void ldv_blast_assert(void)
2202{
2203
2204 {
2205 ERROR: ;
2206#line 6
2207 goto ERROR;
2208}
2209}
2210#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2211extern int __VERIFIER_nondet_int(void) ;
2212#line 373 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2213int ldv_spin = 0;
2214#line 377 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4729/dscv_tempdir/dscv/ri/43_1a/drivers/power/wm831x_backup.c.p"
2215void ldv_check_alloc_flags(gfp_t flags )