4246 switch_default:
4247#line 366
4248 goto switch_break;
4249 } else {
4250 switch_break: ;
4251 }
4252 }
4253 }
4254 }
4255 while_break: ;
4256 }
4257 ldv_module_exit:
4258 {
4259#line 378
4260 exit_elsa_cs();
4261 }
4262 ldv_final:
4263 {
4264#line 381
4265 ldv_check_final_state();
4266 }
4267#line 384
4268 return;
4269}
4270}
4271#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3634/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4272void ldv_blast_assert(void)
4273{
4274
4275 {
4276 ERROR:
4277#line 6
4278 goto ERROR;
4279}
4280}
4281#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3634/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4282extern int __VERIFIER_nondet_int(void) ;
4283#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3634/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4284int ldv_mutex = 1;
4285#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3634/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4286int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )