4774 } else {
4775
4776 }
4777#line 385
4778 goto switch_break;
4779 switch_default:
4780#line 386
4781 goto switch_break;
4782 } else {
4783 switch_break: ;
4784 }
4785 }
4786 }
4787 }
4788 while_break: ;
4789 }
4790 ldv_module_exit:
4791 {
4792#line 395
4793 ldv_check_final_state();
4794 }
4795#line 398
4796 return;
4797}
4798}
4799#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4014/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4800void ldv_blast_assert(void)
4801{
4802
4803 {
4804 ERROR:
4805#line 6
4806 goto ERROR;
4807}
4808}
4809#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4014/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4810extern int __VERIFIER_nondet_int(void) ;
4811#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4014/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4812int ldv_mutex = 1;
4813#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4014/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4814int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )