diff --git a/src/util/lp/lp_utils.h b/src/util/lp/lp_utils.h
index 9d4fd766f..c48acc584 100644
--- a/src/util/lp/lp_utils.h
+++ b/src/util/lp/lp_utils.h
@@ -22,6 +22,7 @@ Revision History:
 #include "util/lp/numeric_pair.h"
 #include "util/debug.h"
 #include <unordered_map>
+#include <unordered_set>
 template <typename C>
 void print_vector(const C & t, std::ostream & out) {
     for (const auto & p : t)
@@ -212,6 +213,19 @@ struct hash<lp::numeric_pair<lp::mpq>> {
         return seed;
     }
 };
+
+inline
+void intersect_set(std::unordered_set<unsigned>& p, const std::unordered_set<unsigned>& w) {
+        for (auto it = p.begin(); it != p.end(); ) {
+            auto iit = it;
+            iit ++;
+            if (w.find(*it) == w.end())
+                p.erase(it);
+            it = iit;
+        }
+    }
+
+
 }
 
 
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index 40ad0fd36..dea03f54c 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -832,30 +832,6 @@ struct solver::imp {
         register_key_mono_in_rooted_monomials(mc, i_mon);        
     }
 
-    void intersect_set(std::unordered_set<unsigned>& p, const std::unordered_set<unsigned>& w) {
-        for (auto it = p.begin(); it != p.end(); ) {
-            auto iit = it;
-            iit ++;
-            if (w.find(*it) == w.end())
-                p.erase(it);
-            it = iit;
-        }
-    }
-
-    void reduce_set_by_checking_proper_containment(std::unordered_set<unsigned>& p,
-                                                   const rooted_mon & rm ) {
-        for (auto it = p.begin(); it != p.end();) {
-            if (lp::is_proper_factor(rm.m_vars, m_rm_table.vec()[*it].m_vars)) {
-                it++;
-                continue;
-            }
-            auto iit = it;
-            iit ++;
-            p.erase(it);
-            it = iit;
-        }
-    }
-
     template <typename T>
     void trace_print_rms(const T& p, std::ostream& out) {
         out << "p = {";
@@ -867,35 +843,7 @@ struct solver::imp {
         out << "\n}";
     }
     
-    // here i is the index of a monomial in m_vector_of_rooted_monomials
-    void find_rooted_monomials_containing_rm(unsigned i_rm) {
-        const auto & rm = m_rm_table.vec()[i_rm];
-       
-        std::unordered_set<unsigned> p = m_rm_table.var_map()[rm[0]];
-        TRACE("nla_solver",
-              tout << "i_rm = " << i_rm << ", rm = ";
-              print_rooted_monomial(rm, tout);
-              tout << "\n rm[0] =" << rm[0] << " var = ";
-              print_var(rm[0], tout);
-              tout << "\n";
-              trace_print_rms(p, tout);
-              );
-        
-        
-        for (unsigned k = 1; k < rm.size(); k++) {
-            intersect_set(p, m_rm_table.var_map()[rm[k]]);
-        }
-        TRACE("nla_solver", trace_print_rms(p, tout););
-        reduce_set_by_checking_proper_containment(p, rm);
-        TRACE("nla_solver", trace_print_rms(p, tout););
-        m_rm_table.m_rooted_factor_to_product[i_rm] = p;
-    }
     
-    void fill_rooted_factor_to_product() {
-        for (unsigned i = 0; i < m_rm_table.vec().size(); i++) {
-            find_rooted_monomials_containing_rm(i);
-        }
-    }
 
     void register_rooted_monomial_containing_vars(unsigned i_rm) {
         TRACE("nla_solver", print_rooted_monomial(m_rm_table.vec()[i_rm], tout););
@@ -925,7 +873,7 @@ struct solver::imp {
             register_monomial_in_tables(i);
 
         fill_rooted_monomials_containing_var();
-        fill_rooted_factor_to_product();
+        m_rm_table.fill_rooted_factor_to_product();
     }
     
     void init_search() {
@@ -1113,8 +1061,8 @@ struct solver::imp {
                     }
                 }
             } else {
-                TRACE("nla_solver", tout << "not a var = " << m_rm_table.m_rooted_factor_to_product[d.index()].size() ;);
-                for (unsigned rm_bd : m_rm_table.m_rooted_factor_to_product[d.index()]) {
+                TRACE("nla_solver", tout << "not a var = " << m_rm_table.factor_to_product()[d.index()].size() ;);
+                for (unsigned rm_bd : m_rm_table.factor_to_product()[d.index()]) {
                     TRACE("nla_solver", );
                     if (order_lemma_on_ac_and_bd(rm , ac, k, m_rm_table.vec()[rm_bd], d)) {
                         return true;
diff --git a/src/util/lp/rooted_mons.h b/src/util/lp/rooted_mons.h
index 5a35ec742..d5b7cc308 100644
--- a/src/util/lp/rooted_mons.h
+++ b/src/util/lp/rooted_mons.h
@@ -19,6 +19,7 @@
   --*/
 
 #pragma once
+#include "util/lp/lp_utils.h"
 namespace nla {
 struct rooted_mon {
     svector<lpvar>   m_vars;
@@ -84,5 +85,56 @@ struct rooted_mon_table {
         return m_rooted_monomials_containing_var;
     }
 
+    std::unordered_map<unsigned, std::unordered_set<unsigned>>& factor_to_product() {
+        return m_rooted_factor_to_product;
+    }
+
+    const std::unordered_map<unsigned, std::unordered_set<unsigned>>& factor_to_product() const {
+        return m_rooted_factor_to_product;
+    }
+
+    void reduce_set_by_checking_proper_containment(std::unordered_set<unsigned>& p,
+                                                   const rooted_mon & rm ) {
+        for (auto it = p.begin(); it != p.end();) {
+            if (lp::is_proper_factor(rm.m_vars, vec()[*it].m_vars)) {
+                it++;
+                continue;
+            }
+            auto iit = it;
+            iit ++;
+            p.erase(it);
+            it = iit;
+        }
+    }
+
+    // here i is the index of a monomial in m_vector_of_rooted_monomials
+    void find_rooted_monomials_containing_rm(unsigned i_rm) {
+        const auto & rm = vec()[i_rm];
+    
+        std::unordered_set<unsigned> p = var_map()[rm[0]];
+        // TRACE("nla_solver",
+        //       tout << "i_rm = " << i_rm << ", rm = ";
+        //       print_rooted_monomial(rm, tout);
+        //       tout << "\n rm[0] =" << rm[0] << " var = ";
+        //       print_var(rm[0], tout);
+        //       tout << "\n";
+        //       trace_print_rms(p, tout);
+        //       );
+    
+    
+        for (unsigned k = 1; k < rm.size(); k++) {
+            intersect_set(p, var_map()[rm[k]]);
+        }
+        // TRACE("nla_solver", trace_print_rms(p, tout););
+        reduce_set_by_checking_proper_containment(p, rm);
+        // TRACE("nla_solver", trace_print_rms(p, tout););
+        factor_to_product()[i_rm] = p;
+    }
+
+    void fill_rooted_factor_to_product() {
+        for (unsigned i = 0; i < vec().size(); i++) {
+            find_rooted_monomials_containing_rm(i);
+        }
+    }
 };
 }