1746#line 266
1747 if (0) {
1748 switch_default:
1749#line 268
1750 goto switch_break;
1751 } else {
1752 switch_break: ;
1753 }
1754 }
1755 }
1756 while_break: ;
1757 }
1758 {
1759#line 306
1760 edac_exit_mce_inject();
1761 }
1762 ldv_final:
1763 {
1764#line 309
1765 ldv_check_final_state();
1766 }
1767#line 312
1768 return;
1769}
1770}
1771#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1772void ldv_blast_assert(void)
1773{
1774
1775 {
1776 ERROR:
1777#line 6
1778 goto ERROR;
1779}
1780}
1781#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1782extern int __VERIFIER_nondet_int(void) ;
1783#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1784int ldv_mutex = 1;
1785#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5313/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1786int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )