diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index 017f1cf77..f26a9a550 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include "math/grobner/grobner.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_ll_pp.h"
 #include "util/ref_util.h"
 
 // #define PROFILE_GB
@@ -121,7 +122,7 @@ void grobner::reset() {
 
 void grobner::display_var(std::ostream & out, expr * var) const {
     if (is_app(var) && to_app(var)->get_num_args() > 0)
-        out << "#" << var->get_id();
+        out << mk_bounded_pp(var, m_manager);
     else
         out << mk_pp(var, m_manager);
 }
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 80687dd18..1293b4546 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -1931,7 +1931,7 @@ namespace smt {
         derived_bound  b(null_theory_var, inf_numeral(0), B_LOWER);
         dependency2new_bound(d, b);
         set_conflict(b, ante, "arith_nl");
-        TRACE("non_linear", for (literal lit : b.m_lits) tout << lit << " "; tout << "\n";); 
+        TRACE("non_linear", for (literal lit : b.m_lits) get_context().display_literal_verbose(tout, lit) << "\n"; tout << "\n";); 
     }
 
     /**
diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp
index 872b8c3e7..a0dfc79cc 100644
--- a/src/smt/theory_array_bapa.cpp
+++ b/src/smt/theory_array_bapa.cpp
@@ -436,7 +436,7 @@ namespace smt {
         {
             context& ctx = th.get_context();
             m_arith_value.init(&ctx);
-            m_max_set_enumeration = 100;
+            m_max_set_enumeration = 4;
         }
 
         ~imp() {
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 6d361bc22..1ab4c823b 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -599,11 +599,14 @@ class solve_eqs_tactic : public tactic {
             hoist_rewriter_star rw(m());
             th_rewriter thrw(m());
             expr_ref tmp(m()), tmp2(m());
+            TRACE("solve_eqs", g.display(tout););
             for (unsigned idx = 0; idx < size; idx++) {
                 checkpoint();
+                if (g.is_decided_unsat()) break;
                 expr* f = g.form(idx);
                 thrw(f, tmp);
                 rw(tmp, tmp2);
+                TRACE("solve_eqs", tout << mk_pp(f, m()) << " " << tmp2 << "\n";);
                 g.update(idx, tmp2, g.pr(idx), g.dep(idx));
             }