293#line 140
294 if (0) {
295 switch_default:
296#line 142
297 goto switch_break;
298 } else {
299 switch_break: ;
300 }
301 }
302 }
303 while_break: ;
304 }
305 {
306#line 154
307 exit_rc_map_terratec_slim_2();
308 }
309 ldv_final:
310 {
311#line 157
312 ldv_check_final_state();
313 }
314#line 160
315 return;
316}
317}
318#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12941/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
319void ldv_blast_assert(void)
320{
321
322 {
323 ERROR:
324#line 6
325 goto ERROR;
326}
327}
328#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12941/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
329extern int __VERIFIER_nondet_int(void) ;
330#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12941/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
331int ldv_mutex = 1;
332#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12941/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
333int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )