4583 } else {
4584
4585 }
4586#line 392
4587 goto switch_break;
4588 switch_default:
4589#line 393
4590 goto switch_break;
4591 } else {
4592 switch_break: ;
4593 }
4594 }
4595 }
4596 }
4597 while_break: ;
4598 }
4599 ldv_module_exit:
4600 {
4601#line 402
4602 ldv_check_final_state();
4603 }
4604#line 405
4605 return;
4606}
4607}
4608#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4161/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4609void ldv_blast_assert(void)
4610{
4611
4612 {
4613 ERROR:
4614#line 6
4615 goto ERROR;
4616}
4617}
4618#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4161/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4619extern int __VERIFIER_nondet_int(void) ;
4620#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4161/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4621int ldv_mutex = 1;
4622#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4161/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4623int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )