3629 switch_default:
3630#line 398
3631 goto switch_break;
3632 } else {
3633 switch_break: ;
3634 }
3635 }
3636 }
3637 }
3638 while_break: ;
3639 }
3640 ldv_module_exit:
3641 {
3642#line 413
3643 warrior_exit();
3644 }
3645 ldv_final:
3646 {
3647#line 416
3648 ldv_check_final_state();
3649 }
3650#line 419
3651 return;
3652}
3653}
3654#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4109/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3655void ldv_blast_assert(void)
3656{
3657
3658 {
3659 ERROR:
3660#line 6
3661 goto ERROR;
3662}
3663}
3664#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4109/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3665extern int __VERIFIER_nondet_int(void) ;
3666#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4109/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3667int ldv_mutex = 1;
3668#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4109/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3669int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )