458#line 167
459 tmp___1 = __VERIFIER_nondet_int();
460 }
461#line 167
462 if (tmp___1 != 0) {
463#line 168
464 goto ldv_19080;
465 } else {
466#line 170
467 goto ldv_19082;
468 }
469 ldv_19082: ;
470 {
471#line 184
472 exit_rc_map_tevii_nec();
473 }
474 ldv_final:
475 {
476#line 187
477 ldv_check_final_state();
478 }
479#line 190
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/9201/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/9201/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
494extern int __VERIFIER_nondet_int(void) ;
495#line 211 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9201/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-tevii-nec.c.p"
496int ldv_spin = 0;
497#line 215 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9201/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-tevii-nec.c.p"
498void ldv_check_alloc_flags(gfp_t flags )