3680 } else {
3681
3682 }
3683#line 278
3684 goto switch_break;
3685 switch_default:
3686#line 279
3687 goto switch_break;
3688 } else {
3689 switch_break: ;
3690 }
3691 }
3692 }
3693 }
3694 while_break: ;
3695 }
3696 ldv_module_exit:
3697 {
3698#line 288
3699 ldv_check_final_state();
3700 }
3701#line 291
3702 return;
3703}
3704}
3705#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3706void ldv_blast_assert(void)
3707{
3708
3709 {
3710 ERROR:
3711#line 6
3712 goto ERROR;
3713}
3714}
3715#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3716extern int __VERIFIER_nondet_int(void) ;
3717#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3718int ldv_mutex = 1;
3719#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4045/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3720int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )