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