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