diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index a0947ea42c8..264c2a08c15 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 044a42e7e62..436dccc6ae5 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -2154,13 +2154,14 @@ void theory_arith<Ext>::set_gb_exhausted() {
 // Scan the grobner basis eqs, and look for inconsistencies.
 template<typename Ext>
 bool theory_arith<Ext>::get_gb_eqs_and_look_for_conflict(ptr_vector<grobner::equation>& 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;