From bf9779cb87d77436cbee73c47644f9837116bd4c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 30 Mar 2020 12:46:18 -0700
Subject: [PATCH] fix #3593

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_core.h | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 9c507eed0..3f0f37d1f 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1276,7 +1276,6 @@ namespace smt {
         expr * rhs2;
         if (m_util.is_to_real(rhs, rhs2) && is_app(rhs2)) { rhs = to_app(rhs2); }
         if (!m_util.is_numeral(rhs)) {
-            UNREACHABLE();
             throw default_exception("malformed atomic constraint");
         }
         theory_var v   = internalize_term_core(lhs);