From 34137cfa0aab5b5ede8353aa6cb8d04b853e97f2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 7 Feb 2019 16:30:49 -0800 Subject: [PATCH] a bug fix in internalize_atom, by NB Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 45f0ea559..e2713b09d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -990,7 +990,7 @@ public: return true; } else { - TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";); + TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";); found_not_handled(atom); return true; } @@ -1780,6 +1780,12 @@ public: for (auto& kv : coeffs) kv.m_value.neg(); } + for (auto const& kv : coeffs) { + theory_var w = kv.m_key; + expr* o = get_enode(w)->get_owner(); + is_int &= a.is_int(o); + } + app_ref atom(m); app_ref t = coeffs2app(coeffs, rational::zero(), is_int); if (lower_bound) {