5072 goto switch_break;
5073 switch_default:
5074#line 290
5075 goto switch_break;
5076 } else {
5077 switch_break: ;
5078 }
5079 }
5080 }
5081 }
5082 while_break: ;
5083 }
5084 {
5085#line 305
5086 bl_trig_exit();
5087 }
5088 ldv_final:
5089 {
5090#line 308
5091 ldv_check_final_state();
5092 }
5093#line 311
5094 return;
5095}
5096}
5097#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12613/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5098void ldv_blast_assert(void)
5099{
5100
5101 {
5102 ERROR:
5103#line 6
5104 goto ERROR;
5105}
5106}
5107#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12613/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5108extern int __VERIFIER_nondet_int(void) ;
5109#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12613/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5110int ldv_mutex = 1;
5111#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12613/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5112int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )