3149 } else {
3150
3151 }
3152#line 187
3153 goto switch_break;
3154 switch_default:
3155#line 188
3156 goto switch_break;
3157 } else {
3158 switch_break: ;
3159 }
3160 }
3161 }
3162 }
3163 while_break: ;
3164 }
3165 ldv_module_exit:
3166 {
3167#line 197
3168 ldv_check_final_state();
3169 }
3170#line 200
3171 return;
3172}
3173}
3174#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3175void ldv_blast_assert(void)
3176{
3177
3178 {
3179 ERROR:
3180#line 6
3181 goto ERROR;
3182}
3183}
3184#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3185extern int __VERIFIER_nondet_int(void) ;
3186#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3187int ldv_mutex = 1;
3188#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4895/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3189int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )