4689 tmp___7 = __VERIFIER_nondet_int();
4690 }
4691 {
4692#line 226
4693 goto switch_default;
4694#line 224
4695 if (0) {
4696 switch_default:
4697#line 226
4698 goto switch_break;
4699 } else {
4700 switch_break: ;
4701 }
4702 }
4703 }
4704 while_break: ;
4705 }
4706 {
4707#line 235
4708 ldv_check_final_state();
4709 }
4710#line 238
4711 return;
4712}
4713}
4714#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13371/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4715void ldv_blast_assert(void)
4716{
4717
4718 {
4719 ERROR:
4720#line 6
4721 goto ERROR;
4722}
4723}
4724#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13371/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4725extern int __VERIFIER_nondet_int(void) ;
4726#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13371/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4727int ldv_mutex = 1;
4728#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13371/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4729int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )