12355 goto switch_break;
12356 switch_default:
12357#line 652
12358 goto switch_break;
12359 } else {
12360 switch_break: ;
12361 }
12362 }
12363 }
12364 }
12365 while_break: ;
12366 }
12367 {
12368#line 669
12369 friq_exit();
12370 }
12371 ldv_final:
12372 {
12373#line 672
12374 ldv_check_final_state();
12375 }
12376#line 675
12377 return;
12378}
12379}
12380#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16804/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
12381void ldv_blast_assert(void)
12382{
12383
12384 {
12385 ERROR:
12386#line 6
12387 goto ERROR;
12388}
12389}
12390#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16804/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
12391extern int __VERIFIER_nondet_int(void) ;
12392#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16804/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
12393int ldv_mutex = 1;
12394#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16804/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
12395int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )