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