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