diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index d2871df6b..61b99fb50 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -50,15 +50,15 @@ bool nla_grobner::internalize_gb_eq(equation* ) {
 }
 
 void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std::queue<lpvar> & q) {
-    SASSERT(m_active_vars.contains(j) == false);
+    SASSERT(!c().active_var_set_contains(j));
     const auto& matrix = c().m_lar_solver.A_r();
-    m_active_vars.insert(j);
+    c().insert_to_active_var_set(j);
     for (auto & s : matrix.m_columns[j]) {
         unsigned row = s.var();
         if (m_rows.contains(row)) continue;
         m_rows.insert(row);
         for (auto& rc : matrix.m_rows[row]) {
-            if (m_active_vars.contains(rc.var()))
+            if (c().active_var_set_contains(rc.var()))
                 continue;
             q.push(rc.var());
         }
@@ -71,7 +71,7 @@ void nla_grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, std
     for (auto fcn : factorization_factory_imp(m, c())) {
         for (const factor& fc: fcn) {
             lpvar j = var(fc);
-            if (! m_active_vars.contains(j))
+            if (! c().active_var_set_contains(j))
                 add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
         }
     }            
@@ -88,7 +88,7 @@ void nla_grobner::find_nl_cluster() {
     while (!q.empty()) {
         unsigned j = q.front();        
         q.pop();
-        if (m_active_vars.contains(j))
+        if (c().active_var_set_contains(j))
             continue;
         add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
     }
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index 9bc21ab98..12d4f16ff 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -82,7 +82,6 @@ class nla_grobner : common {
     equation_vector                              m_equations_to_unfreeze;
     equation_vector                              m_equations_to_delete;    
     lp::int_set                                  m_rows;
-    lp::int_set                                  m_active_vars;
     unsigned                                     m_num_of_equations;
     grobner_stats                                m_stats;
     equation_set                                 m_processed;