From f784120312799b5c9e19c9a756b8ffc6d08bc5a4 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 14 Mar 2019 14:45:47 -0700 Subject: [PATCH] rebase with Z3Prover/master Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index d1536629e..ee40a0916 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -91,7 +91,7 @@ std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostr std::ostream& lar_solver::print_values(std::ostream& out) const { for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) { const numeric_pair & rp = m_mpq_lar_core_solver.m_r_x[i]; - out << this->get_column_name(i) << " -> " << rp << "\n"; + out << this->get_variable_name(i) << " -> " << rp << "\n"; } return out; } @@ -1273,7 +1273,7 @@ void lar_solver::get_model(std::unordered_map & variable_values) delta /= mpq(2); break; } - TRACE("get_model", tout << get_column_name(i) << " := " << x << "\n";); + TRACE("get_model", tout << this->get_variable_name(j) << " := " << x << "\n";); if (!column_corresponds_to_term(j)) variable_values[j] = x; }