From 5dc1337476ce434670887e969ffd7a72eb08332e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 28 Nov 2018 13:49:53 -0800 Subject: [PATCH] fix #1984 - already fixed in private branch, but wasn't propagated to master Signed-off-by: Nikolaj Bjorner --- src/smt/arith_eq_solver.cpp | 9 +++------ src/smt/theory_lra.cpp | 7 +++++++ 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp index 4b1c6e4a6..677132804 100644 --- a/src/smt/arith_eq_solver.cpp +++ b/src/smt/arith_eq_solver.cpp @@ -608,8 +608,8 @@ bool arith_eq_solver::solve_integer_equations_gcd( return false; } live.erase(live.begin()+live_pos); - for (j = 0; j < live.size(); ++j) { - row& r = rows[live[j]]; + for (unsigned l : live) { + row& r = rows[l]; if (!r[i].is_zero()) { substitute(r, r0, i); gcd_normalize(r); @@ -625,10 +625,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( TRACE("arith_eq_solver", tout << ((live.size()<=1)?"solved ":"incomplete check ") << live.size() << "\n"; - for (unsigned i = 0; i < live.size(); ++i) { - print_row(tout, rows[live[i]]); - } - ); + for (unsigned l : live) print_row(tout, rows[l]); ); return true; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0b25aa626..818a20d93 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -323,6 +323,10 @@ class theory_lra::imp { m_solver->settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test; m_solver->settings().set_random_seed(ctx().get_fparams().m_random_seed); m_lia = alloc(lp::int_solver, m_solver.get()); + get_one(true); + get_zero(true); + get_one(false); + get_zero(false); } void ensure_nra() { @@ -346,6 +350,7 @@ class theory_lra::imp { var = m_solver->add_var(v, true); m_theory_var2var_index.setx(v, var, UINT_MAX); m_var_index2theory_var.setx(var, v, UINT_MAX); + TRACE("arith", tout << v << " internal: " << var << "\n";); m_var_trail.push_back(v); add_def_constraint(m_solver->add_var_bound(var, lp::GE, rational(c))); add_def_constraint(m_solver->add_var_bound(var, lp::LE, rational(c))); @@ -662,6 +667,7 @@ class theory_lra::imp { m_has_int |= is_int(v); m_theory_var2var_index.setx(v, result, UINT_MAX); m_var_index2theory_var.setx(result, v, UINT_MAX); + TRACE("arith", tout << v << " internal: " << result << "\n";); m_var_trail.push_back(v); } return result; @@ -828,6 +834,7 @@ class theory_lra::imp { SASSERT(!m_left_side.empty()); vi = m_solver->add_term(m_left_side); m_theory_var2var_index.setx(v, vi, UINT_MAX); + TRACE("arith", tout << v << " internal: " << vi << "\n";); if (m_solver->is_term(vi)) { m_term_index2theory_var.setx(m_solver->adjust_term_index(vi), v, UINT_MAX); }