7512 goto switch_break;
7513 switch_default:
7514#line 687
7515 goto switch_break;
7516 } else {
7517 switch_break: ;
7518 }
7519 }
7520 }
7521 }
7522 while_break: ;
7523 }
7524 {
7525#line 705
7526 epia_exit();
7527 }
7528 ldv_final:
7529 {
7530#line 708
7531 ldv_check_final_state();
7532 }
7533#line 711
7534 return;
7535}
7536}
7537#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16801/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7538void ldv_blast_assert(void)
7539{
7540
7541 {
7542 ERROR:
7543#line 6
7544 goto ERROR;
7545}
7546}
7547#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16801/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7548extern int __VERIFIER_nondet_int(void) ;
7549#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16801/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7550int ldv_mutex = 1;
7551#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16801/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7552int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )