mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 20:35:51 +00:00
Code Activity

improve tracing

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-07-29 11:06:47 -07:00
parent 9dbd8d3d46
commit b9483d0aff
3 changed files with 19 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/nla_core.cpp
View file

@ -275,14 +275,15 @@ std::ostream& core::print_monomial_with_vars(const monomial& m, std::ostream& ou
std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out) const {
out << "expl: ";
unsigned i = 0;
for (auto &p : exp) {
out << "(" << p.second << ")";
m_lar_solver.print_constraint_indices_only_customized(p.second,
[this](lpvar j) { return var_str(j);},
out);
out << " ";
if (++i < exp.size())
out << " ";
}
out << "\n";
return out;
}