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