348#line 210
349 if (0) {
350 switch_default:
351#line 212
352 goto switch_break;
353 } else {
354 switch_break: ;
355 }
356 }
357 }
358 while_break: ;
359 }
360 {
361#line 224
362 exit_rc_map_imon_mce();
363 }
364 ldv_final:
365 {
366#line 227
367 ldv_check_final_state();
368 }
369#line 230
370 return;
371}
372}
373#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12900/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
374void ldv_blast_assert(void)
375{
376
377 {
378 ERROR:
379#line 6
380 goto ERROR;
381}
382}
383#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12900/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
384extern int __VERIFIER_nondet_int(void) ;
385#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12900/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
386int ldv_mutex = 1;
387#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12900/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
388int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )