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