437#line 149
438 tmp___1 = __VERIFIER_nondet_int();
439 }
440#line 149
441 if (tmp___1 != 0) {
442#line 150
443 goto ldv_19080;
444 } else {
445#line 152
446 goto ldv_19082;
447 }
448 ldv_19082: ;
449 {
450#line 166
451 exit_rc_map_pinnacle_pctv_hd();
452 }
453 ldv_final:
454 {
455#line 169
456 ldv_check_final_state();
457 }
458#line 172
459 return;
460}
461}
462#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9183/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
463void ldv_blast_assert(void)
464{
465
466 {
467 ERROR: ;
468#line 6
469 goto ERROR;
470}
471}
472#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9183/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
473extern int __VERIFIER_nondet_int(void) ;
474#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9183/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-pinnacle-pctv-hd.c.p"
475int ldv_spin = 0;
476#line 197 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9183/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-pinnacle-pctv-hd.c.p"
477void ldv_check_alloc_flags(gfp_t flags )