330#line 180
331 if (0) {
332 switch_default:
333#line 182
334 goto switch_break;
335 } else {
336 switch_break: ;
337 }
338 }
339 }
340 while_break: ;
341 }
342 {
343#line 194
344 exit_rc_map_encore_enltv();
345 }
346 ldv_final:
347 {
348#line 197
349 ldv_check_final_state();
350 }
351#line 200
352 return;
353}
354}
355#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
356void ldv_blast_assert(void)
357{
358
359 {
360 ERROR:
361#line 6
362 goto ERROR;
363}
364}
365#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
366extern int __VERIFIER_nondet_int(void) ;
367#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
368int ldv_mutex = 1;
369#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12889/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
370int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )