3327#line 535
3328 tmp___1 = __VERIFIER_nondet_int();
3329 }
3330#line 535
3331 if (tmp___1 != 0) {
3332#line 536
3333 goto ldv_15304;
3334 } else {
3335#line 538
3336 goto ldv_15306;
3337 }
3338 ldv_15306: ;
3339 {
3340#line 629
3341 w1_f29_exit();
3342 }
3343 ldv_final:
3344 {
3345#line 632
3346 ldv_check_final_state();
3347 }
3348#line 635
3349 return;
3350}
3351}
3352#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4908/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3353void ldv_blast_assert(void)
3354{
3355
3356 {
3357 ERROR: ;
3358#line 6
3359 goto ERROR;
3360}
3361}
3362#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4908/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3363extern int __VERIFIER_nondet_int(void) ;
3364#line 656 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4908/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2408.c.p"
3365int ldv_spin = 0;
3366#line 660 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4908/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2408.c.p"
3367void ldv_check_alloc_flags(gfp_t flags )