4467 goto switch_break;
4468 switch_default:
4469#line 214
4470 goto switch_break;
4471 } else {
4472 switch_break: ;
4473 }
4474 }
4475 }
4476 }
4477 while_break: ;
4478 }
4479 {
4480#line 228
4481 dm_zero_exit();
4482 }
4483 ldv_final:
4484 {
4485#line 231
4486 ldv_check_final_state();
4487 }
4488#line 234
4489 return;
4490}
4491}
4492#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4705/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4493void ldv_blast_assert(void)
4494{
4495
4496 {
4497 ERROR:
4498#line 6
4499 goto ERROR;
4500}
4501}
4502#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4705/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4503extern int __VERIFIER_nondet_int(void) ;
4504#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4705/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4505int ldv_mutex = 1;
4506#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4705/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4507int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )