501#line 235
502 tmp___1 = __VERIFIER_nondet_int();
503 }
504#line 235
505 if (tmp___1 != 0) {
506#line 236
507 goto ldv_19080;
508 } else {
509#line 238
510 goto ldv_19082;
511 }
512 ldv_19082: ;
513 {
514#line 252
515 exit_rc_map_imon_pad();
516 }
517 ldv_final:
518 {
519#line 255
520 ldv_check_final_state();
521 }
522#line 258
523 return;
524}
525}
526#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9159/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
527void ldv_blast_assert(void)
528{
529
530 {
531 ERROR: ;
532#line 6
533 goto ERROR;
534}
535}
536#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9159/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
537extern int __VERIFIER_nondet_int(void) ;
538#line 279 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9159/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-imon-pad.c.p"
539int ldv_spin = 0;
540#line 283 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/9159/dscv_tempdir/dscv/ri/43_1a/drivers/media/rc/keymaps/rc-imon-pad.c.p"
541void ldv_check_alloc_flags(gfp_t flags )