mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 12:11:23 +00:00
Code Activity

better tracing

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-03-08 09:27:12 -08:00
parent 0dbfcad560
commit 4963108277
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/util/lp/nla_solver.cpp
View file

@ -287,7 +287,7 @@ struct solver::imp {
template <typename T> template <typename T>
std::ostream& print_product(const T & m, std::ostream& out) const { std::ostream& print_product(const T & m, std::ostream& out) const {
for (unsigned k = 0; k < m.size(); k++) { for (unsigned k = 0; k < m.size(); k++) {
out << m_lar_solver.get_variable_name(m[k]); out << "(" << m_lar_solver.get_variable_name(m[k]) << "=" << vvr(m[k]) << ")";
if (k + 1 < m.size()) out << "*"; if (k + 1 < m.size()) out << "*";
} }
return out; return out;
@ -2215,7 +2215,8 @@ struct solver::imp {
if (v.is_zero()) if (v.is_zero())
continue; continue;
if (order_lemma_on_factor(rm, ac, k, derived)) { if (order_lemma_on_factor(rm, ac, k, derived)) {
TRACE("nla_solver", print_lemma(tout););
return true; return true;
} }
} }