From 293b0b8cc25400bbb37e6ab6a4bd6ce6fcfde080 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Jul 2020 12:49:18 -0700 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- 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 bbbade83f..88696629a 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1251,7 +1251,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)) { - SASSERT(false); throw default_exception("malformed atomic constraint"); } theory_var v = internalize_term_core(lhs);