2857 goto switch_break;
2858 switch_default:
2859#line 216
2860 goto switch_break;
2861 } else {
2862 switch_break: ;
2863 }
2864 }
2865 }
2866 }
2867 while_break: ;
2868 }
2869 {
2870#line 231
2871 sp_exit();
2872 }
2873 ldv_final:
2874 {
2875#line 234
2876 ldv_check_final_state();
2877 }
2878#line 237
2879 return;
2880}
2881}
2882#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/229/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2883void ldv_blast_assert(void)
2884{
2885
2886 {
2887 ERROR:
2888#line 6
2889 goto ERROR;
2890}
2891}
2892#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/229/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2893extern int __VERIFIER_nondet_int(void) ;
2894#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/229/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2895int ldv_mutex = 1;
2896#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/229/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2897int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )