3239 } else {
3240
3241 }
3242#line 340
3243 goto switch_break;
3244 switch_default:
3245#line 341
3246 goto switch_break;
3247 } else {
3248 switch_break: ;
3249 }
3250 }
3251 }
3252 }
3253 while_break: ;
3254 }
3255 ldv_module_exit:
3256 {
3257#line 350
3258 ldv_check_final_state();
3259 }
3260#line 353
3261 return;
3262}
3263}
3264#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1707/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3265void ldv_blast_assert(void)
3266{
3267
3268 {
3269 ERROR:
3270#line 6
3271 goto ERROR;
3272}
3273}
3274#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1707/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3275extern int __VERIFIER_nondet_int(void) ;
3276#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1707/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3277int ldv_mutex = 1;
3278#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1707/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3279int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )