diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index 11bebf6c5..c6f7b4cbb 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -59,15 +59,19 @@ void grobner::del_equation(equation * eq) {
     m_to_process.erase(eq);
     SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
     m_equations_to_delete[eq->m_bidx] = 0;
-    ptr_vector<monomial>::iterator it1  = eq->m_monomials.begin();
-    ptr_vector<monomial>::iterator end1 = eq->m_monomials.end();
-    for (; it1 != end1; ++it1) {
-        monomial * m = *it1;
-        del_monomial(m);
-    }
+    del_monomials(eq->m_monomials);
     dealloc(eq);
 }
 
+void grobner::del_monomials(ptr_vector<monomial>& ms) {
+    ptr_vector<monomial>::iterator it  = ms.begin();
+    ptr_vector<monomial>::iterator end = ms.end();
+    for (; it != end; ++it) {
+        del_monomial(*it);
+    }
+    ms.reset();
+}
+
 void grobner::del_monomial(monomial * m) {
     ptr_vector<expr>::iterator it2  = m->m_vars.begin();
     ptr_vector<expr>::iterator end2 = m->m_vars.end();
@@ -436,16 +440,18 @@ void grobner::merge_monomials(ptr_vector<monomial> & monomials) {
     unsigned sz = monomials.size();
     if (sz == 0)
         return;
+    ptr_vector<monomial>& to_delete = m_tmp_monomials;
+    to_delete.reset();
     for (unsigned i = 1; i < sz; ++i) {
         monomial * m1 = monomials[j];
         monomial * m2 = monomials[i];
         if (is_eq_monomial_body(m1, m2)) {
             m1->m_coeff += m2->m_coeff;
-            del_monomial(m2);
+            to_delete.push_back(m2);
         } 
         else {
             if (m1->m_coeff.is_zero())
-                del_monomial(m1); // cancelled
+                to_delete.push_back(m1);
             else
                 j++;
             monomials[j] = m2;
@@ -454,10 +460,11 @@ void grobner::merge_monomials(ptr_vector<monomial> & monomials) {
     SASSERT(j < sz);
     monomial * m1 = monomials[j];
     if (m1->m_coeff.is_zero())
-        del_monomial(m1); // cancelled
+        to_delete.push_back(m1);
     else
         j++;
     monomials.shrink(j);
+    del_monomials(to_delete);    
     TRACE("grobner", tout << "after merging monomials:\n"; display_monomials(tout, monomials.size(), monomials.c_ptr()); tout << "\n";);
 }
 
@@ -649,6 +656,7 @@ grobner::equation * grobner::simplify(equation const * source, equation * target
                     target->m_lc = false;
                 mul_append(1, source, coeff, rest, new_monomials);
                 del_monomial(curr);
+                target->m_monomials[i] = 0;
             }
             else {
                 target->m_monomials[j] = curr;
diff --git a/src/math/grobner/grobner.h b/src/math/grobner/grobner.h
index 7d58115e3..32a4423a6 100644
--- a/src/math/grobner/grobner.h
+++ b/src/math/grobner/grobner.h
@@ -126,6 +126,8 @@ protected:
 
     void del_equations(unsigned old_size);
 
+    void del_monomials(ptr_vector<monomial>& monomials);
+
     void unfreeze_equations(unsigned old_size);
 
     void del_equation(equation * eq);