From a9d22d7409553ec0c0076ecdc3301a558bafee5e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Feb 2020 14:09:40 -0800 Subject: [PATCH] fix #2918 Signed-off-by: Nikolaj Bjorner --- src/math/lp/gomory.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index 5148dedc0..46f745d03 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -298,7 +298,7 @@ public: mpq t = abs(ceil(p.coeff())); if (t > m_abs_max) m_abs_max = t; } - m_big_number = m_abs_max; // .expt(2); + m_big_number = m_abs_max.expt(2); #endif mpq one_min_m_f = 1 - m_f; for (const auto & p : m_row) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 596179145..bf807dc6e 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -142,6 +142,11 @@ struct goal2sat::imp { else if (m.is_false(t)) { l = sign ? mk_true() : ~mk_true(); } + else if (!is_app(t)) { + std::ostringstream strm; + strm << mk_ismt2_pp(t, m); + throw_op_not_handled(strm.str()); + } else { bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t); sat::bool_var v = m_solver.add_var(ext);