5215 } else {
5216
5217 }
5218#line 535
5219 goto switch_break;
5220 switch_default:
5221#line 536
5222 goto switch_break;
5223 } else {
5224 switch_break: ;
5225 }
5226 }
5227 }
5228 }
5229 while_break: ;
5230 }
5231 ldv_module_exit:
5232 {
5233#line 545
5234 ldv_check_final_state();
5235 }
5236#line 548
5237 return;
5238}
5239}
5240#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6255/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5241void ldv_blast_assert(void)
5242{
5243
5244 {
5245 ERROR:
5246#line 6
5247 goto ERROR;
5248}
5249}
5250#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6255/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5251extern int __VERIFIER_nondet_int(void) ;
5252#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6255/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5253int ldv_mutex = 1;
5254#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6255/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5255int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )