diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index c6f7b4cbb..3bca8c3e7 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -440,7 +440,8 @@ void grobner::merge_monomials(ptr_vector<monomial> & monomials) {
     unsigned sz = monomials.size();
     if (sz == 0)
         return;
-    ptr_vector<monomial>& to_delete = m_tmp_monomials;
+    SASSERT(&m_del_monomials != &monomials);
+    ptr_vector<monomial>& to_delete = m_del_monomials;
     to_delete.reset();
     for (unsigned i = 1; i < sz; ++i) {
         monomial * m1 = monomials[j];
diff --git a/src/math/grobner/grobner.h b/src/math/grobner/grobner.h
index 32a4423a6..fa200f70d 100644
--- a/src/math/grobner/grobner.h
+++ b/src/math/grobner/grobner.h
@@ -110,6 +110,7 @@ protected:
     };
     svector<scope>          m_scopes;
     ptr_vector<monomial>    m_tmp_monomials;
+    ptr_vector<monomial>    m_del_monomials;
     ptr_vector<expr>        m_tmp_vars1;
     ptr_vector<expr>        m_tmp_vars2;
     unsigned                m_num_new_equations; // temporary variable
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index d1444bd88..565181877 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1524,9 +1524,7 @@ namespace smt {
 
         numeral a_ij, curr_a_ij, coeff, curr_coeff;
         inf_numeral min_gain, max_gain, curr_min_gain, curr_max_gain;
-#ifdef _TRACE
         unsigned round = 0;
-#endif
         max_min_t result = OPTIMIZED;
         has_shared = false;
         unsigned max_efforts = 10 + (ctx.get_random_value() % 20);
@@ -1535,7 +1533,9 @@ namespace smt {
             theory_var x_i = null_theory_var;
             max_gain.reset();
             min_gain.reset();
-            TRACE("opt", tout << "round: " << (round++) << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout););
+            ++round;
+
+            TRACE("opt", tout << "round: " << round << ", max: " << max << "\n"; display_row(tout, r, true); tout << "state:\n"; display(tout););
             typename vector<row_entry>::const_iterator it  = r.begin_entries();
             typename vector<row_entry>::const_iterator end = r.end_entries();
             for (; it != end; ++it) {  
@@ -1561,7 +1561,7 @@ namespace smt {
                     best_efforts++;
                 }
                 else if (curr_x_i == null_theory_var) {
-                    TRACE("opt", tout << "unbounded\n";);
+                    TRACE("opt", tout << "v" << curr_x_j << " is unrestricted by other variables\n";);
                     // we can increase/decrease curr_x_j as much as we want.
                     x_i   = null_theory_var; // unbounded
                     x_j   = curr_x_j;
@@ -1592,7 +1592,7 @@ namespace smt {
             }
 
             TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n";
-                  tout << "best efforts: " << best_efforts << "\n";);
+                  tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";);
             
             if (x_j == null_theory_var) {
                 TRACE("opt", tout << "row is " << (max ? "maximized" : "minimized") << "\n";
@@ -1610,6 +1610,7 @@ namespace smt {
                 // can increase/decrease x_j as much as we want.
                 
                 if (inc && upper(x_j)) {
+                    if (max_gain.is_zero()) return BEST_EFFORT;
                     SASSERT(!unbounded_gain(max_gain));
                     update_value(x_j, max_gain);
                     TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";);
@@ -1618,6 +1619,7 @@ namespace smt {
                     continue;
                 }
                 if (!inc && lower(x_j)) {
+                    if (max_gain.is_zero()) return BEST_EFFORT;
                     SASSERT(!unbounded_gain(max_gain));
                     SASSERT(max_gain.is_pos());
                     max_gain.neg();