5894#line 496
5895 LDV_IN_INTERRUPT = 1;
5896 }
5897#line 502
5898 goto switch_break;
5899 switch_default:
5900#line 503
5901 goto switch_break;
5902 } else {
5903 switch_break: ;
5904 }
5905 }
5906 }
5907 }
5908 while_break: ;
5909 }
5910 ldv_module_exit:
5911 {
5912#line 512
5913 ldv_check_final_state();
5914 }
5915#line 515
5916 return;
5917}
5918}
5919#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4172/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5920void ldv_blast_assert(void)
5921{
5922
5923 {
5924 ERROR:
5925#line 6
5926 goto ERROR;
5927}
5928}
5929#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4172/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5930extern int __VERIFIER_nondet_int(void) ;
5931#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4172/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5932int ldv_mutex = 1;
5933#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4172/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5934int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )