3061 goto switch_break;
3062 switch_default:
3063#line 198
3064 goto switch_break;
3065 } else {
3066 switch_break: ;
3067 }
3068 }
3069 }
3070 }
3071 while_break: ;
3072 }
3073 {
3074#line 213
3075 ts_exit();
3076 }
3077 ldv_final:
3078 {
3079#line 216
3080 ldv_check_final_state();
3081 }
3082#line 219
3083 return;
3084}
3085}
3086#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3087void ldv_blast_assert(void)
3088{
3089
3090 {
3091 ERROR:
3092#line 6
3093 goto ERROR;
3094}
3095}
3096#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3097extern int __VERIFIER_nondet_int(void) ;
3098#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3099int ldv_mutex = 1;
3100#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/232/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3101int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )