mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

more streamlined diagnostics to prepare for #5106

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-15 16:23:35 -07:00
parent d03fdf5fed
commit ff0de59a70
4 changed files with 13 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/lp/lar_solver.cpp
View file

@ -1252,6 +1252,15 @@ namespace lp {
// ********** print region start
std::ostream& lar_solver::display(std::ostream& out) const {
out << constraints();
print_terms(out);
pp(out).print();
for (unsigned j = 0; j < number_of_vars(); j++)
print_column_info(j, out);
return out;
}
std::ostream& lar_solver::print_terms(std::ostream& out) const {
for (auto it : m_terms) {
print_term(*it, out) << "\n";