From 67497ba897b1216983298cbdb4161892250b23d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Mar 2020 09:37:54 -0800 Subject: [PATCH] fix #3131 Signed-off-by: Nikolaj Bjorner --- src/math/simplex/model_based_opt.cpp | 2 +- src/qe/qe_arith.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index 4053c41b7..74f808f1d 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -824,7 +824,7 @@ namespace opt { rational val(c); SASSERT(r.m_vars.empty()); r.m_vars.append(coeffs.size(), coeffs.c_ptr()); - bool is_int_row = true; + bool is_int_row = !coeffs.empty(); std::sort(r.m_vars.begin(), r.m_vars.end(), var::compare()); for (auto const& c : coeffs) { val += m_var2value[c.m_id] * c.m_coeff; diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index c141e8112..fa2871a85 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -67,6 +67,7 @@ namespace qe { CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";); SASSERT(m.is_true(val));); + TRACE("opt", tout << mk_pp(lit, m) << " " << a.is_lt(lit) << " " << a.is_gt(lit) << "\n";); bool is_not = m.is_not(lit, lit); if (is_not) { mul.neg();