3546 switch_default:
3547#line 895
3548 goto switch_break;
3549 } else {
3550 switch_break: ;
3551 }
3552 }
3553 }
3554 }
3555 while_break: ;
3556 }
3557 ldv_module_exit:
3558 {
3559#line 914
3560 waltop_exit();
3561 }
3562 ldv_final:
3563 {
3564#line 917
3565 ldv_check_final_state();
3566 }
3567#line 920
3568 return;
3569}
3570}
3571#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/236/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3572void ldv_blast_assert(void)
3573{
3574
3575 {
3576 ERROR:
3577#line 6
3578 goto ERROR;
3579}
3580}
3581#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/236/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3582extern int __VERIFIER_nondet_int(void) ;
3583#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/236/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3584int ldv_mutex = 1;
3585#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/236/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3586int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )