diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp
index 111592eeb..6261953c5 100644
--- a/src/math/lp/nex_creator.cpp
+++ b/src/math/lp/nex_creator.cpp
@@ -593,7 +593,7 @@ void nex_creator::process_map_pair(nex*e, const rational& coeff, nex_sum & sum,
     }
     bool e_is_old = allocated_nexs.find(e) != allocated_nexs.end();
     if (!e_is_old) {
-        m_allocated.push_back(e);
+        add_to_allocated(e);
     }
     if (e->is_mul()) {
         e->to_mul().m_coeff = coeff;
diff --git a/src/math/lp/nex_creator.h b/src/math/lp/nex_creator.h
index a5bfaaf37..33e8497a1 100644
--- a/src/math/lp/nex_creator.h
+++ b/src/math/lp/nex_creator.h
@@ -155,7 +155,10 @@ public:
     const std::unordered_map<lpvar, unsigned>& powers() const { return m_powers; }
     std::unordered_map<lpvar, unsigned>& powers() { return m_powers; }
 
-    void add_to_allocated(nex* r) { m_allocated.push_back(r); }
+    void add_to_allocated(nex* r) {
+        m_allocated.push_back(r);
+        CTRACE("grobner_stats_d", m_allocated.size() % 1000 == 0, tout << "m_allocated.size() = " << m_allocated.size() << "\n";);
+    }
 
     // NSB: we can use region allocation, but still need to invoke destructor 
     // because of 'rational' (and m_children in nex_mul unless we get rid of this)
@@ -163,6 +166,7 @@ public:
         for (unsigned j = sz; j < m_allocated.size(); j++)
             dealloc(m_allocated[j]);
         m_allocated.resize(sz);
+        TRACE("grobner_stats_d", tout << "m_allocated.size() = " << m_allocated.size() << "\n";);
     }
 
     void clear() {
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 3ed157190..cc469ea23 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -250,6 +250,7 @@ grobner_core::equation_set const& grobner_core::equations() {
 
 void grobner_core::reset() {
     del_equations(0);
+    m_nex_creator.pop(0);
     SASSERT(m_equations_to_delete.empty());    
     m_to_superpose.reset();
     m_to_simplify.reset();
@@ -617,7 +618,7 @@ void grobner_core::superpose(equation * eq1, equation * eq2) {
         return;
     }
     equation* eq = alloc(equation);
-    TRACE("grobner_d", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2););
+    TRACE("grobner_d", tout << "eq1="; display_equation(tout, *eq1) << "eq2="; display_equation(tout, *eq2););    
     init_equation(eq, expr_superpose(eq1->expr(), eq2->expr(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep()));
     if (m_nex_creator.gt(eq->expr(), eq1->expr()) || m_nex_creator.gt(eq->expr(), eq2->expr()) ||
         equation_is_too_complex(eq)) {