2530 goto switch_break;
2531 switch_default:
2532#line 163
2533 goto switch_break;
2534 } else {
2535 switch_break: ;
2536 }
2537 }
2538 }
2539 }
2540 while_break: ;
2541 }
2542 {
2543#line 175
2544 keytouch_exit();
2545 }
2546 ldv_final:
2547 {
2548#line 178
2549 ldv_check_final_state();
2550 }
2551#line 181
2552 return;
2553}
2554}
2555#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/201/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2556void ldv_blast_assert(void)
2557{
2558
2559 {
2560 ERROR:
2561#line 6
2562 goto ERROR;
2563}
2564}
2565#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/201/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2566extern int __VERIFIER_nondet_int(void) ;
2567#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/201/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2568int ldv_mutex = 1;
2569#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/201/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2570int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )