307#line 153
308 if (0) {
309 switch_default:
310#line 155
311 goto switch_break;
312 } else {
313 switch_break: ;
314 }
315 }
316 }
317 while_break: ;
318 }
319 {
320#line 167
321 exit_rc_map_msi_digivox_iii();
322 }
323 ldv_final:
324 {
325#line 170
326 ldv_check_final_state();
327 }
328#line 173
329 return;
330}
331}
332#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12915/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
333void ldv_blast_assert(void)
334{
335
336 {
337 ERROR:
338#line 6
339 goto ERROR;
340}
341}
342#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12915/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
343extern int __VERIFIER_nondet_int(void) ;
344#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12915/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
345int ldv_mutex = 1;
346#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12915/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
347int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )