10625 goto switch_break;
10626 switch_default:
10627#line 1444
10628 goto switch_break;
10629 } else {
10630 switch_break: ;
10631 }
10632 }
10633 }
10634 }
10635 while_break: ;
10636 }
10637 {
10638#line 1465
10639 kcapi_exit();
10640 }
10641 ldv_final:
10642 {
10643#line 1468
10644 ldv_check_final_state();
10645 }
10646#line 1471
10647 return;
10648}
10649}
10650#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3398/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
10651void ldv_blast_assert(void)
10652{
10653
10654 {
10655 ERROR:
10656#line 6
10657 goto ERROR;
10658}
10659}
10660#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3398/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
10661extern int __VERIFIER_nondet_int(void) ;
10662#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3398/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10663int ldv_mutex = 1;
10664#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/3398/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10665int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )