450#line 360
451 if (0) {
452 switch_default:
453#line 362
454 goto switch_break;
455 } else {
456 switch_break: ;
457 }
458 }
459 }
460 while_break: ;
461 }
462 {
463#line 374
464 exit_rc_map_rc5_hauppauge_new();
465 }
466 ldv_final:
467 {
468#line 377
469 ldv_check_final_state();
470 }
471#line 380
472 return;
473}
474}
475#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
476void ldv_blast_assert(void)
477{
478
479 {
480 ERROR:
481#line 6
482 goto ERROR;
483}
484}
485#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
486extern int __VERIFIER_nondet_int(void) ;
487#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
488int ldv_mutex = 1;
489#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12899/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
490int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )