4417 tmp___7 = __VERIFIER_nondet_int();
4418 }
4419 {
4420#line 115
4421 goto switch_default;
4422#line 113
4423 if (0) {
4424 switch_default:
4425#line 115
4426 goto switch_break;
4427 } else {
4428 switch_break: ;
4429 }
4430 }
4431 }
4432 while_break: ;
4433 }
4434 {
4435#line 124
4436 ldv_check_final_state();
4437 }
4438#line 127
4439 return;
4440}
4441}
4442#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7565/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4443void ldv_blast_assert(void)
4444{
4445
4446 {
4447 ERROR:
4448#line 6
4449 goto ERROR;
4450}
4451}
4452#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7565/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4453extern int __VERIFIER_nondet_int(void) ;
4454#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7565/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4455int ldv_mutex = 1;
4456#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7565/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4457int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )