466#line 175
467 tmp___1 = __VERIFIER_nondet_int();
468 }
469#line 175
470 if (tmp___1 != 0) {
471#line 176
472 goto ldv_19080;
473 } else {
474#line 178
475 goto ldv_19082;
476 }
477 ldv_19082: ;
478 {
479#line 192
480 exit_rc_map_nebula();
481 }
482 ldv_final:
483 {
484#line 195
485 ldv_check_final_state();
486 }
487#line 198
488 return;
489}
490}
491#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9176/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
492void ldv_blast_assert(void)
493{
494
495 {
496 ERROR: ;
497#line 6
498 goto ERROR;
499}
500}
501#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9176/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
502extern int __VERIFIER_nondet_int(void) ;
503#line 219 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9176/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-nebula.c.p"
504int ldv_spin = 0;
505#line 223 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9176/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-nebula.c.p"
506void ldv_check_alloc_flags(gfp_t flags )