diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 95d50ad34..9f92c9910 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -220,18 +220,24 @@ bool grobner_core::compute_basis_step() {
         return true;
     }
     m_stats.m_compute_steps++;
-    simplify_using_to_superpose(*eq);
-
-    if (equation_is_too_complex(eq))
+    unsigned mem_size = m_nex_creator.size();
+    simplify_eq_by_using_to_superpose(*eq);
+    if (equation_is_too_complex(eq)) {
+        m_nex_creator.pop(mem_size);
         return false;
+    }
+    mem_size = m_nex_creator.size();
     if (!simplify_to_superpose_with_eq(eq)) {
+        m_nex_creator.pop(mem_size);
         return false;
     }
     TRACE("grobner", tout << "eq = "; display_equation(tout, *eq););
+    mem_size = m_nex_creator.size();
     superpose(eq);
-    if (equation_is_too_complex(eq)) {
+    if (equation_is_too_complex(eq)) {        
         TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";);
         del_equation(eq);
+        m_nex_creator.pop(mem_size);
         return false;
     }
     insert_to_superpose(eq);
@@ -259,7 +265,7 @@ grobner_core::equation* grobner_core::pick_next() {
     return r;
 }
 
-void grobner_core::simplify_using_to_superpose(equation& eq) {
+void grobner_core::simplify_eq_by_using_to_superpose(equation& eq) {
     bool simplified;
     TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
     do {
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 72cb887d1..d56abaa4f 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -121,7 +121,7 @@ private:
     bool compute_basis_step();
 
     bool simplify_source_target(equation const& source, equation& target);
-    void simplify_using_to_superpose(equation &);
+    void simplify_eq_by_using_to_superpose(equation &);
     bool simplify_target_monomials(equation const& source, equation& target);
     void process_simplified_target(equation* target, ptr_buffer<equation>& to_remove);    
     bool simplify_to_superpose_with_eq(equation*);