From ff265235c1d01b72d0065fd5b7e75bf57d3724f4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Jun 2022 08:19:52 -0700 Subject: [PATCH] adjust trace output --- src/math/grobner/grobner.cpp | 3 +++ src/smt/theory_arith_nl.h | 7 ++++--- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp index a0947ea42..264c2a08c 100644 --- a/src/math/grobner/grobner.cpp +++ b/src/math/grobner/grobner.cpp @@ -116,10 +116,13 @@ void grobner::reset() { } void grobner::display_var(std::ostream & out, expr * var) const { + out << "#" << var->get_id(); +#if 0 if (is_app(var) && to_app(var)->get_num_args() > 0) out << mk_bounded_pp(var, m_manager); else out << mk_pp(var, m_manager); +#endif } void grobner::display_vars(std::ostream & out, unsigned num_vars, expr * const * vars) const { diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 044a42e7e..436dccc6a 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -2154,13 +2154,14 @@ void theory_arith::set_gb_exhausted() { // Scan the grobner basis eqs, and look for inconsistencies. template bool theory_arith::get_gb_eqs_and_look_for_conflict(ptr_vector& eqs, grobner& gb) { - TRACE("grobner", ); eqs.reset(); gb.get_equations(eqs); - TRACE("grobner_bug", tout << "after gb\n";); + TRACE("grobner", tout << "after gb\n"; + for (grobner::equation* eq : eqs) + gb.display_equation(tout, *eq); + ); for (grobner::equation* eq : eqs) { - TRACE("grobner_bug", gb.display_equation(tout, *eq);); if (is_inconsistent(eq, gb) || is_inconsistent2(eq, gb)) { TRACE("grobner", tout << "inconsistent: "; gb.display_equation(tout, *eq);); return true;