458#line 172
459 tmp___1 = __VERIFIER_nondet_int();
460 }
461#line 172
462 if (tmp___1 != 0) {
463#line 173
464 goto ldv_19080;
465 } else {
466#line 175
467 goto ldv_19082;
468 }
469 ldv_19082: ;
470 {
471#line 189
472 exit_rc_it913x_v2_map();
473 }
474 ldv_final:
475 {
476#line 192
477 ldv_check_final_state();
478 }
479#line 195
480 return;
481}
482}
483#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9162/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
484void ldv_blast_assert(void)
485{
486
487 {
488 ERROR: ;
489#line 6
490 goto ERROR;
491}
492}
493#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9162/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
494extern int __VERIFIER_nondet_int(void) ;
495#line 216 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9162/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-it913x-v2.c.p"
496int ldv_spin = 0;
497#line 220 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9162/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-it913x-v2.c.p"
498void ldv_check_alloc_flags(gfp_t flags )