5312 }
5313 ldv_22926: ;
5314 ldv_22928:
5315 {
5316#line 438
5317 tmp___0 = __VERIFIER_nondet_int();
5318 }
5319#line 438
5320 if (tmp___0 != 0) {
5321#line 439
5322 goto ldv_22927;
5323 } else {
5324#line 441
5325 goto ldv_22929;
5326 }
5327 ldv_22929: ;
5328
5329 {
5330#line 452
5331 ldv_check_final_state();
5332 }
5333#line 455
5334 return;
5335}
5336}
5337#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5509/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5338void ldv_blast_assert(void)
5339{
5340
5341 {
5342 ERROR: ;
5343#line 6
5344 goto ERROR;
5345}
5346}
5347#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5509/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5348extern int __VERIFIER_nondet_int(void) ;
5349#line 476 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5509/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/ring_sw.c.p"
5350int ldv_spin = 0;
5351#line 480 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5509/dscv_tempdir/dscv/ri/43_1a/drivers/staging/iio/ring_sw.c.p"
5352void ldv_check_alloc_flags(gfp_t flags )