4679 } else {
4680
4681 }
4682#line 382
4683 goto switch_break;
4684 switch_default:
4685#line 383
4686 goto switch_break;
4687 } else {
4688 switch_break: ;
4689 }
4690 }
4691 }
4692 }
4693 while_break: ;
4694 }
4695 ldv_module_exit:
4696 {
4697#line 392
4698 ldv_check_final_state();
4699 }
4700#line 395
4701 return;
4702}
4703}
4704#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6233/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4705void ldv_blast_assert(void)
4706{
4707
4708 {
4709 ERROR:
4710#line 6
4711 goto ERROR;
4712}
4713}
4714#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6233/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4715extern int __VERIFIER_nondet_int(void) ;
4716#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6233/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4717int ldv_mutex = 1;
4718#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6233/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4719int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )