16142 switch_default:
16143#line 1792
16144 goto switch_break;
16145 } else {
16146 switch_break: ;
16147 }
16148 }
16149 }
16150 }
16151 while_break: ;
16152 }
16153 ldv_module_exit:
16154 {
16155#line 1806
16156 tcm_loop_fabric_exit();
16157 }
16158 ldv_final:
16159 {
16160#line 1809
16161 ldv_check_final_state();
16162 }
16163#line 1812
16164 return;
16165}
16166}
16167#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17463/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
16168void ldv_blast_assert(void)
16169{
16170
16171 {
16172 ERROR:
16173#line 6
16174 goto ERROR;
16175}
16176}
16177#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17463/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
16178extern int __VERIFIER_nondet_int(void) ;
16179#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17463/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
16180int ldv_mutex = 1;
16181#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/17463/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
16182int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )