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

rebase with Z3Prover/master

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-03-14 14:45:47 -07:00
parent cbe920756b
commit f784120312
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/util/lp/lar_solver.cpp
View file

@ -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<mpq> & 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<var_index, mpq> & 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;
}