14797 goto switch_break;
14798 switch_default:
14799#line 4179
14800 goto switch_break;
14801 } else {
14802 switch_break: ;
14803 }
14804 }
14805 }
14806 }
14807 while_break: ;
14808 }
14809 {
14810#line 4223
14811 vivi_exit();
14812 }
14813 ldv_final:
14814 {
14815#line 4226
14816 ldv_check_final_state();
14817 }
14818#line 4229
14819 return;
14820}
14821}
14822#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/15067/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
14823void ldv_blast_assert(void)
14824{
14825
14826 {
14827 ERROR:
14828#line 6
14829 goto ERROR;
14830}
14831}
14832#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/15067/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
14833extern int __VERIFIER_nondet_int(void) ;
14834#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/15067/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14835int ldv_mutex = 1;
14836#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/15067/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
14837int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )