5132 } else {
5133
5134 }
5135#line 405
5136 goto switch_break;
5137 switch_default:
5138#line 406
5139 goto switch_break;
5140 } else {
5141 switch_break: ;
5142 }
5143 }
5144 }
5145 }
5146 while_break: ;
5147 }
5148 ldv_module_exit:
5149 {
5150#line 415
5151 ldv_check_final_state();
5152 }
5153#line 418
5154 return;
5155}
5156}
5157#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4170/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5158void ldv_blast_assert(void)
5159{
5160
5161 {
5162 ERROR:
5163#line 6
5164 goto ERROR;
5165}
5166}
5167#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4170/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5168extern int __VERIFIER_nondet_int(void) ;
5169#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4170/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5170int ldv_mutex = 1;
5171#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4170/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5172int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )