mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3749

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-04 14:45:29 -07:00
parent 8d59355b88
commit 7838e99f47
1 changed files with 13 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/smt/theory_lra.cpp
View file

@ -978,15 +978,19 @@ class theory_lra::imp {
if (!st.offset().is_zero()) { if (!st.offset().is_zero()) {
m_left_side.push_back(std::make_pair(st.offset(), get_one(a.is_int(term)))); m_left_side.push_back(std::make_pair(st.offset(), get_one(a.is_int(term))));
} }
vi = lp().add_term(m_left_side, v); if (m_left_side.empty()) {
SASSERT(lp::tv::is_term(vi)); vi = lp().add_var(v, a.is_int(term));
TRACE("arith_verbose", add_def_constraint(lp().add_var_bound(vi, lp::GE, rational(0)));
tout << "v" << v << " := " << mk_pp(term, m) add_def_constraint(lp().add_var_bound(vi, lp::LE, rational(0)));
<< " slack: " << vi << " scopes: " << m_scopes.size() << "\n"; }
lp().print_term(lp().get_term(vi), tout) << "\n";); else {
} vi = lp().add_term(m_left_side, v);
else { SASSERT(lp::tv::is_term(vi));
SASSERT(lp::tv::is_term(vi) || a.is_to_real(term)); 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; rational val;