2538 goto switch_break;
2539 switch_default:
2540#line 154
2541 goto switch_break;
2542 } else {
2543 switch_break: ;
2544 }
2545 }
2546 }
2547 }
2548 while_break: ;
2549 }
2550 {
2551#line 166
2552 elecom_exit();
2553 }
2554 ldv_final:
2555 {
2556#line 169
2557 ldv_check_final_state();
2558 }
2559#line 172
2560 return;
2561}
2562}
2563#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/193/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2564void ldv_blast_assert(void)
2565{
2566
2567 {
2568 ERROR:
2569#line 6
2570 goto ERROR;
2571}
2572}
2573#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/193/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2574extern int __VERIFIER_nondet_int(void) ;
2575#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/193/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2576int ldv_mutex = 1;
2577#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/193/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2578int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )