From 7838e99f4793c7543d422bf9a61c1dfc3d7d698a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 4 Apr 2020 14:45:29 -0700 Subject: [PATCH] fix #3749 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index efcef6b2f..d22e46f19 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -978,15 +978,19 @@ class theory_lra::imp { if (!st.offset().is_zero()) { m_left_side.push_back(std::make_pair(st.offset(), get_one(a.is_int(term)))); } - vi = lp().add_term(m_left_side, v); - SASSERT(lp::tv::is_term(vi)); - TRACE("arith_verbose", - tout << "v" << v << " := " << mk_pp(term, m) - << " slack: " << vi << " scopes: " << m_scopes.size() << "\n"; - lp().print_term(lp().get_term(vi), tout) << "\n";); - } - else { - SASSERT(lp::tv::is_term(vi) || a.is_to_real(term)); + if (m_left_side.empty()) { + vi = lp().add_var(v, a.is_int(term)); + add_def_constraint(lp().add_var_bound(vi, lp::GE, rational(0))); + add_def_constraint(lp().add_var_bound(vi, lp::LE, rational(0))); + } + else { + vi = lp().add_term(m_left_side, v); + SASSERT(lp::tv::is_term(vi)); + TRACE("arith_verbose", + tout << "v" << v << " := " << mk_pp(term, m) + << " slack: " << vi << " scopes: " << m_scopes.size() << "\n"; + lp().print_term(lp().get_term(vi), tout) << "\n";); + } } rational val;