462#line 171
463 tmp___1 = __VERIFIER_nondet_int();
464 }
465#line 171
466 if (tmp___1 != 0) {
467#line 172
468 goto ldv_19080;
469 } else {
470#line 174
471 goto ldv_19082;
472 }
473 ldv_19082: ;
474 {
475#line 188
476 exit_rc_map_videomate_k100();
477 }
478 ldv_final:
479 {
480#line 191
481 ldv_check_final_state();
482 }
483#line 194
484 return;
485}
486}
487#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9207/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
488void ldv_blast_assert(void)
489{
490
491 {
492 ERROR: ;
493#line 6
494 goto ERROR;
495}
496}
497#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9207/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
498extern int __VERIFIER_nondet_int(void) ;
499#line 215 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9207/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-videomate-m1f.c.p"
500int ldv_spin = 0;
501#line 219 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9207/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-videomate-m1f.c.p"
502void ldv_check_alloc_flags(gfp_t flags )