4708 tmp___7 = __VERIFIER_nondet_int();
4709 }
4710 {
4711#line 210
4712 goto switch_default;
4713#line 208
4714 if (0) {
4715 switch_default:
4716#line 210
4717 goto switch_break;
4718 } else {
4719 switch_break: ;
4720 }
4721 }
4722 }
4723 while_break: ;
4724 }
4725 {
4726#line 219
4727 ldv_check_final_state();
4728 }
4729#line 222
4730 return;
4731}
4732}
4733#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13383/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4734void ldv_blast_assert(void)
4735{
4736
4737 {
4738 ERROR:
4739#line 6
4740 goto ERROR;
4741}
4742}
4743#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13383/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4744extern int __VERIFIER_nondet_int(void) ;
4745#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13383/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4746int ldv_mutex = 1;
4747#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13383/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4748int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )