mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-28 05:58:55 +00:00
Code Activity

improve printing

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-08-29 19:12:57 +08:00
parent 08c9953a36
commit 18714ce020
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/util/lp/niil_solver.cpp
View file

@ -532,12 +532,13 @@ struct solver::imp {
if (j == m.m_v) { if (j == m.m_v) {
monomial = true; monomial = true;
print_monomial(m, out); print_monomial(m, out);
out << " = " << m_lar_solver.get_column_value(j) << "\n";; out << " = " << m_lar_solver.get_column_value(j);;
break; break;
} }
} }
if (!monomial) if (!monomial)
out << m_lar_solver.get_column_name(j) << " = " << m_lar_solver.get_column_value(j); out << m_lar_solver.get_column_name(j) << " = " << m_lar_solver.get_column_value(j);
out <<";";
return out; return out;
} }