diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index eb91f75b8..8ca8401e7 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1576,8 +1576,8 @@ void core::display_matrix_of_m_rows(std::ostream & out) const {
     }
 }
 
-void core::init_nex_grobner(nex_creator & nc) {   
-    TRACE("grobner", tout << "m_rows.size() = " << m_rows.size() << "\n";);
+void core::init_nex_grobner(nex_creator & nc) {
+    m_nex_grobner.init();
     set_active_vars_weights(nc);
     for (unsigned i : m_rows) {
         m_nex_grobner.add_row(m_lar_solver.A_r().m_rows[i]);
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 78e79afa7..bb4a43e8f 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -36,7 +36,6 @@ grobner::grobner(core *c, intervals *s)
 
 void grobner::grobner_lemmas() {
     c().lp_settings().stats().m_grobner_calls++;
-    m_gc.reset();
     m_reported = 0;
     TRACE("grobner", tout << "before:\n"; display(tout););
     m_gc.compute_basis_loop();
@@ -87,6 +86,10 @@ Each step proceeds as follows:
     - simplify A using a
 */
 
+void grobner::init() {
+    m_gc.reset();
+}
+
 bool grobner_core::compute_basis_loop() {
     while (!done()) {
         if (compute_basis_step()) {
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index a9d1d8a2a..81e429007 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -212,13 +212,13 @@ public:
 private:
     void prepare_rows_and_active_vars();
     void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j,  svector<lpvar>& q);
-    void init();
     std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
     void display_matrix(std::ostream & out) const;
     std::ostream& display(std::ostream& out) const { return m_gc.display(out); }
 public:
     void add_row(const vector<lp::row_cell<rational>> & row);
     void check_eq(grobner_core::equation*);
+    void init();
     nex_creator& get_nex_creator() { return m_nex_creator; }
 }; // end of grobner
 }