2683 goto switch_break;
2684 switch_default:
2685#line 172
2686 goto switch_break;
2687 } else {
2688 switch_break: ;
2689 }
2690 }
2691 }
2692 }
2693 while_break: ;
2694 }
2695 {
2696#line 186
2697 ks_exit();
2698 }
2699 ldv_final:
2700 {
2701#line 189
2702 ldv_check_final_state();
2703 }
2704#line 192
2705 return;
2706}
2707}
2708#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/200/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2709void ldv_blast_assert(void)
2710{
2711
2712 {
2713 ERROR:
2714#line 6
2715 goto ERROR;
2716}
2717}
2718#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/200/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2719extern int __VERIFIER_nondet_int(void) ;
2720#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/200/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2721int ldv_mutex = 1;
2722#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/200/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2723int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )