5701 switch_default:
5702#line 750
5703 goto switch_break;
5704 } else {
5705 switch_break: ;
5706 }
5707 }
5708 }
5709 }
5710 while_break: ;
5711 }
5712 ldv_module_exit:
5713 {
5714#line 767
5715 soft_exit();
5716 }
5717 ldv_final:
5718 {
5719#line 770
5720 ldv_check_final_state();
5721 }
5722#line 773
5723 return;
5724}
5725}
5726#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1177/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5727void ldv_blast_assert(void)
5728{
5729
5730 {
5731 ERROR:
5732#line 6
5733 goto ERROR;
5734}
5735}
5736#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1177/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5737extern int __VERIFIER_nondet_int(void) ;
5738#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1177/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5739int ldv_mutex = 1;
5740#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1177/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5741int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )