5777 } else {
5778
5779 }
5780#line 647
5781 goto switch_break;
5782 switch_default:
5783#line 648
5784 goto switch_break;
5785 } else {
5786 switch_break: ;
5787 }
5788 }
5789 }
5790 }
5791 while_break: ;
5792 }
5793 ldv_module_exit:
5794 {
5795#line 657
5796 ldv_check_final_state();
5797 }
5798#line 660
5799 return;
5800}
5801}
5802#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14195/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5803void ldv_blast_assert(void)
5804{
5805
5806 {
5807 ERROR:
5808#line 6
5809 goto ERROR;
5810}
5811}
5812#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14195/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5813extern int __VERIFIER_nondet_int(void) ;
5814#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14195/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5815int ldv_mutex = 1;
5816#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14195/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5817int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )