481#line 203
482 tmp___1 = __VERIFIER_nondet_int();
483 }
484#line 203
485 if (tmp___1 != 0) {
486#line 204
487 goto ldv_19080;
488 } else {
489#line 206
490 goto ldv_19082;
491 }
492 ldv_19082: ;
493 {
494#line 220
495 exit_rc_map();
496 }
497 ldv_final:
498 {
499#line 223
500 ldv_check_final_state();
501 }
502#line 226
503 return;
504}
505}
506#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9138/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
507void ldv_blast_assert(void)
508{
509
510 {
511 ERROR: ;
512#line 6
513 goto ERROR;
514}
515}
516#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9138/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
517extern int __VERIFIER_nondet_int(void) ;
518#line 247 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9138/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-nec.c.p"
519int ldv_spin = 0;
520#line 251 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9138/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-dib0700-nec.c.p"
521void ldv_check_alloc_flags(gfp_t flags )