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