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