diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp
index 3b4532be6..7398475fa 100644
--- a/src/util/lp/emonomials.cpp
+++ b/src/util/lp/emonomials.cpp
@@ -24,15 +24,6 @@
 
 namespace nla {
 
-    void emonomials::inc_canonical() {
-        ++m_canonical;
-        if (m_canonical == 0) {
-            for (auto& svt : m_canonized) {
-                svt.m_canonical = 0;
-            }
-            ++m_canonical;
-        }
-    }
 
     void emonomials::inc_visited() const {
         ++m_visited;
@@ -55,11 +46,12 @@ namespace nla {
         unsigned old_sz = m_lim[m_lim.size() - n];
         for (unsigned i = m_monomials.size(); i-- > old_sz; ) {
             monomial const& m = m_monomials[i];
+            remove_cg(i, m);
             m_var2index[m.var()] = UINT_MAX;
             lpvar last_var = UINT_MAX;
             for (lpvar v : m.vars()) {
                 if (v != last_var) {
-                    remove_var2monomials(v, i);
+                    remove_cell(m_use_lists[v], i);
                     last_var = v;
                 }
             }
@@ -70,9 +62,9 @@ namespace nla {
         m_lim.shrink(m_lim.size() - n);
     }
 
-    void emonomials::remove_var2monomials(lpvar v, unsigned mIndex) {
-        cell*& cur_head = m_use_lists[v].m_head;
-        cell*& cur_tail = m_use_lists[v].m_tail;
+    void emonomials::remove_cell(head_tail& v, unsigned mIndex) {
+        cell*& cur_head = v.m_head;
+        cell*& cur_tail = v.m_tail;
         cell* old_head = cur_head->m_next;
         if (old_head == cur_head) {
             cur_head = nullptr;
@@ -84,23 +76,21 @@ namespace nla {
         }
     }
 
-    void emonomials::insert_var2monomials(lpvar v, unsigned mIndex) {
-        m_use_lists.reserve(v + 1);
-        cell*& cur_head = m_use_lists[v].m_head;
-        cell*& cur_tail = m_use_lists[v].m_tail;
+    void emonomials::insert_cell(head_tail& v, unsigned mIndex) {
+        cell*& cur_head = v.m_head;
+        cell*& cur_tail = v.m_tail;
         cell* new_head = new (m_region) cell(mIndex, cur_head);
         cur_head = new_head;
         if (!cur_tail) cur_tail = new_head;
         cur_tail->m_next = new_head;
     }
 
-    void emonomials::merge_var2monomials(lpvar root, lpvar other) {
-        if (root == other) return;
-        m_use_lists.reserve(std::max(root, other) + 1);
-        cell*& root_head = m_use_lists[root].m_head;
-        cell*& root_tail = m_use_lists[root].m_tail;
-        cell* other_head = m_use_lists[other].m_head;
-        cell* other_tail = m_use_lists[other].m_tail;
+    void emonomials::merge_cells(head_tail& root, head_tail& other) {
+        if (&root == &other) return;
+        cell*& root_head = root.m_head;
+        cell*& root_tail = root.m_tail;
+        cell* other_head = other.m_head;
+        cell* other_tail = other.m_tail;
         if (root_head == nullptr) {
             root_head = other_head;
             root_tail = other_tail;
@@ -116,12 +106,12 @@ namespace nla {
         }
     }
 
-    void emonomials::unmerge_var2monomials(lpvar root, lpvar other) {
-        if (root == other) return;
-        cell*& root_head = m_use_lists[root].m_head;
-        cell*& root_tail = m_use_lists[root].m_tail;
-        cell* other_head = m_use_lists[other].m_head;
-        cell* other_tail = m_use_lists[other].m_tail;
+    void emonomials::unmerge_cells(head_tail& root, head_tail& other) {
+        if (&root == &other) return;
+        cell*& root_head = root.m_head;
+        cell*& root_tail = root.m_tail;
+        cell* other_head = other.m_head;
+        cell* other_tail = other.m_tail;
         if (other_head == nullptr) {
             // no-op
         }
@@ -142,6 +132,112 @@ namespace nla {
         return m_use_lists[v].m_head;
     }
 
+    signed_vars const* emonomials::find_canonical(svector<lpvar> const& vars) const { 
+        // find a unique key for dummy monomial
+        lpvar v = m_var2index.size();
+        for (unsigned i = 0; i < m_var2index.size(); ++i) {
+            if (m_var2index[i] == UINT_MAX) {
+                v = i;
+                break;
+            }
+        }
+        unsigned idx = m_monomials.size();
+        m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr()));
+        m_canonized.push_back(signed_vars_ts(v, idx));
+        m_var2index.setx(v, idx, UINT_MAX);
+        do_canonize(m_monomials[idx]);
+        signed_vars const* result = nullptr;
+        lpvar w; 
+        if (m_cg_table.find(v, w)) {
+            SASSERT(w != v);
+            result = &m_canonized[m_var2index[w]];
+        }
+        m_var2index[v] = UINT_MAX;
+        m_monomials.pop_back();
+        m_canonized.pop_back(); // NB. relies on the pointer m_canonized not to change.
+        return result;
+    }
+
+
+    void emonomials::remove_cg(lpvar v) {
+        cell* c = m_use_lists[v].m_head;
+        cell* first = c;
+        inc_visited();
+        do {
+            unsigned idx = c->m_index;
+            c = c->m_next;
+            monomial const& m = m_monomials[idx];
+            if (!is_visited(m)) {
+                set_visited(m);
+                remove_cg(idx, m);
+            }
+        }
+        while (c != first);
+    }
+
+    void emonomials::remove_cg(unsigned idx, monomial const& m) {
+        signed_vars_ts& sv = m_canonized[idx];
+        unsigned next = sv.m_next;
+        unsigned prev = sv.m_prev;
+        
+        lpvar u = m.var(), w;
+        // equivalence class of u:
+        if (m_cg_table.find(u, w) && w == u) {
+            m_cg_table.erase(u);
+            // insert other representative:
+            if (prev != idx) {
+                m_cg_table.insert(m_monomials[prev].var());
+            }
+        }
+        if (prev != idx) {
+            m_canonized[next].m_prev = prev;
+            m_canonized[prev].m_next = next;
+            sv.m_next = idx;
+            sv.m_prev = idx;
+        }
+    }
+
+    /**
+       \brief insert canonized monomials using v into a congruence table.
+       Prior to insertion, the monomials are canonized according to the current
+       variable equivalences. The canonized monomials (signed_vars) are considered
+       in the same equivalence class if they have the same set of representative
+       variables. Their signs may differ.       
+    */
+    void emonomials::insert_cg(lpvar v) {
+        cell* c = m_use_lists[v].m_head;
+        cell* first = c;
+        inc_visited();
+        do {
+            unsigned idx = c->m_index;
+            c = c->m_next;
+            monomial const& m = m_monomials[idx];
+            if (!is_visited(m)) {
+                set_visited(m);
+                insert_cg(idx, m);
+            }
+        }
+        while (c != first);
+    }
+
+    void emonomials::insert_cg(unsigned idx, monomial const& m) {
+        canonize(m);
+        lpvar v = m.var(), w;
+        if (m_cg_table.find(v, w)) {
+            SASSERT(w != v);
+            unsigned idxr = m_var2index[w];
+            // Insert idx to the right of idxr
+            m_canonized[idx].m_prev  = idxr;
+            m_canonized[idx].m_next  = m_canonized[idxr].m_next;
+            m_canonized[idxr].m_next = idx;
+        }
+        else {
+            m_cg_table.insert(v);
+            SASSERT(m_canonized[idx].m_next == idx);
+            SASSERT(m_canonized[idx].m_prev == idx);
+        }        
+    }
+
     void emonomials::set_visited(monomial const& m) const {
         m_canonized[m_var2index[m.var()]].m_visited = m_visited;
     }
@@ -150,48 +246,40 @@ namespace nla {
         return m_visited == m_canonized[m_var2index[m.var()]].m_visited;
     }
 
-
     /**
        \brief insert a new monomial.
 
        Assume that the variables are canonical, that is, not equal in current
-       context so another variable. To support equal in current context we
-       could track sign information in monomials, or ensure that insert_var2monomials 
-       works on the equivalence class roots.
+       context so another variable. The monomial is inserted into a congruence
+       class of equal up-to var_eqs monomials.
      */
     void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) {
         unsigned idx = m_monomials.size();
         m_monomials.push_back(monomial(v, sz, vs));
-        m_canonized.push_back(signed_vars_ts());
+        m_canonized.push_back(signed_vars_ts(v, idx));
         lpvar last_var = UINT_MAX;
         for (unsigned i = 0; i < sz; ++i) {
             lpvar w = vs[i];
             SASSERT(m_ve.is_root(w));
             if (w != last_var) {
-                insert_var2monomials(w, idx);
+                m_use_lists.reserve(w + 1);
+                insert_cell(m_use_lists[w], idx);
                 last_var = w; 
             }
         }
         SASSERT(m_ve.is_root(v));
         m_var2index.setx(v, idx, UINT_MAX);
+        insert_cg(idx, m_monomials[idx]);
     }
 
-    signed_vars const& emonomials::canonize(monomial const& mon) const {
+    void emonomials::do_canonize(monomial const& mon) const {
         unsigned index = m_var2index[mon.var()];
-        if (m_canonized[index].m_canonical != m_canonical) {        
-            m_vars.reset();
-            bool sign = false;
-            for (lpvar v : mon) {
-                signed_var sv = m_ve.find(v);
-                m_vars.push_back(sv.var());
-                sign ^= sv.sign();
-            }
-            m_canonized[index].set_vars(m_vars.size(), m_vars.c_ptr());
-            m_canonized[index].set_sign(sign);
-            m_canonized[index].set_var(mon.var());
-            m_canonized[index].m_canonical = m_canonical;
+        signed_vars& svs = m_canonized[index];
+        svs.reset();
+        for (lpvar v : mon) {
+            svs.push_var(m_ve.find(v));
         }
-        return m_canonized[index];
+        svs.done_push();
     }
 
     bool emonomials::canonize_divides(monomial const& m1, monomial const& m2) const {
@@ -242,21 +330,22 @@ namespace nla {
     }
 
     void emonomials::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) {
-        if (!r2.sign() && m_ve.find(~r2) != m_ve.find(r1)) {
-            merge_var2monomials(r2.var(), r1.var());
-        }        
-        inc_canonical();
+        // no-op
     }
 
     void emonomials::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) {
-        // skip
+        if (!r2.sign() && m_ve.find(~r2) != m_ve.find(r1)) {
+            m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1);
+            rehash_cg(r1.var()); 
+            merge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]);
+        }   
     }
 
     void emonomials::unmerge_eh(signed_var r2, signed_var r1) {
         if (!r2.sign() && m_ve.find(~r2) != m_ve.find(r1)) {
-            unmerge_var2monomials(r2.var(), r1.var());            
+            unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]);            
+            rehash_cg(r1.var());
         }        
-        inc_canonical();
     }
 
    std::ostream& emonomials::display(std::ostream& out) const {
diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h
index 8f1135104..76b1242a7 100644
--- a/src/util/lp/emonomials.h
+++ b/src/util/lp/emonomials.h
@@ -36,17 +36,18 @@ namespace nla {
         svector<lpvar>  m_vars;
         bool            m_sign;
     public:
-        signed_vars() : m_sign(false) {}
+        signed_vars(lpvar v) : m_var(v), m_sign(false) {}
         lpvar var() const { return m_var; }
         svector<lpvar> const& vars() const { return m_vars; }
+        svector<lp::var_index>::const_iterator begin() const { return vars().begin(); }
+        svector<lp::var_index>::const_iterator end() const { return vars().end(); }
         unsigned size() const { return m_vars.size(); }
         lpvar operator[](unsigned i) const { return m_vars[i]; }
         bool sign() const { return m_sign; }
-        void set_sign(bool s) { m_sign = s; }
-        void set_var(lpvar v) { m_var = v; }
-        void set_vars(unsigned n, lpvar const* vars) {
-            m_vars.reset();
-            m_vars.append(n, vars);
+        rational rsign() const { return rational(m_sign ? -1 : 1); }
+        void reset() { m_sign = false; m_vars.reset(); }
+        void push_var(signed_var sv) { m_sign ^= sv.sign(); m_vars.push_back(sv.var()); }
+        void done_push() {
             std::sort(m_vars.begin(), m_vars.end());
         }
         std::ostream& display(std::ostream& out) const {
@@ -61,15 +62,6 @@ namespace nla {
 
 
     class emonomials : public var_eqs_merge_handler {
-        /**
-           \brief private fields used by emonomials for maintaining state of canonized monomials.
-        */
-        class signed_vars_ts : public signed_vars {
-        public:
-            signed_vars_ts(): m_canonical(0), m_visited(0) {}
-            unsigned m_canonical;
-            unsigned m_visited;
-        };
 
         /**
            \brief singly-lined cyclic list of monomial indices where variable occurs.
@@ -90,24 +82,64 @@ namespace nla {
             cell* m_tail;
         };
 
-        var_eqs&                m_ve;
-        vector<monomial>        m_monomials;     // set of monomials
-        unsigned_vector         m_lim;           // backtracking point
-        unsigned_vector         m_var2index;     // var_mIndex -> mIndex
-        unsigned                m_canonical;     // timestamp of last merge
-        mutable unsigned        m_visited;       // timestamp of visited monomials during pf_iterator
-        region                  m_region;        // region for allocating linked lists
-        mutable vector<signed_vars_ts>  m_canonized;     // canonized versions of signed variables
-        mutable svector<lpvar>       m_vars;          // temporary vector of variables
-        mutable svector<head_tail>   m_use_lists;     // use list of monomials where variables occur.
 
-        void inc_canonical();
+        /**
+           \brief private fields used by emonomials for maintaining state of canonized monomials.
+        */
+        class signed_vars_ts : public signed_vars {
+        public:
+            signed_vars_ts(lpvar v, unsigned idx): signed_vars(v), m_next(idx), m_prev(idx), m_visited(0) {}
+            unsigned m_next;                    // next congruent node.
+            unsigned m_prev;                    // previous congruent node
+            mutable unsigned m_visited;
+        };
+
+        struct hash_canonical {
+            emonomials& em;
+            hash_canonical(emonomials& em): em(em) {}
+
+            unsigned operator()(lpvar v) const {
+                auto const& vec = em.m_canonized[em.m_var2index[v]].vars();
+                return string_hash(reinterpret_cast<char const*>(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10);
+            }
+        };
+
+        struct eq_canonical {
+            emonomials& em;
+            eq_canonical(emonomials& em): em(em) {}
+            bool operator()(lpvar u, lpvar v) const {
+                auto const& uvec = em.m_canonized[em.m_var2index[u]].vars();
+                auto const& vvec = em.m_canonized[em.m_var2index[v]].vars();
+                return uvec == vvec;
+            }
+        };
+
+        var_eqs&                        m_ve;
+        mutable vector<monomial>        m_monomials;     // set of monomials
+        mutable unsigned_vector         m_var2index;     // var_mIndex -> mIndex
+        unsigned_vector                 m_lim;           // backtracking point
+        mutable unsigned                m_visited;       // timestamp of visited monomials during pf_iterator
+        region                          m_region;        // region for allocating linked lists
+        mutable vector<signed_vars_ts>  m_canonized;     // canonized versions of signed variables
+        mutable svector<head_tail>      m_use_lists;     // use list of monomials where variables occur.
+        hash_canonical                  m_cg_hash;
+        eq_canonical                    m_cg_eq;
+        hashtable<lpvar, hash_canonical, eq_canonical> m_cg_table; // congruence (canonical) table.
+
         void inc_visited() const;
 
-        void remove_var2monomials(lpvar v, unsigned mIndex);
-        void insert_var2monomials(lpvar v, unsigned mIndex);
-        void merge_var2monomials(lpvar root, lpvar other);
-        void unmerge_var2monomials(lpvar root, lpvar other);
+        void remove_cell(head_tail& v, unsigned mIndex);
+        void insert_cell(head_tail& v, unsigned mIndex);
+        void merge_cells(head_tail& root, head_tail& other);
+        void unmerge_cells(head_tail& root, head_tail& other);
+
+        void remove_cg(lpvar v);
+        void insert_cg(lpvar v);
+        void insert_cg(unsigned idx, monomial const& m);
+        void remove_cg(unsigned idx, monomial const& m);
+        void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); }
+
+        void do_canonize(monomial const& m) const; 
 
         cell* head(lpvar v) const;
         void set_visited(monomial const& m) const;
@@ -119,7 +151,15 @@ namespace nla {
            push and pop on emonomials calls push/pop on var_eqs, so no 
            other calls to push/pop to the var_eqs should take place. 
          */
-        emonomials(var_eqs& ve): m_ve(ve), m_canonical(1), m_visited(0) { m_ve.set_merge_handler(this); }
+        emonomials(var_eqs& ve): 
+            m_ve(ve), 
+            m_visited(0), 
+            m_cg_hash(*this),
+            m_cg_eq(*this),
+            m_cg_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_cg_hash, m_cg_eq),
+            canonical(*this) { 
+            m_ve.set_merge_handler(this); 
+        }
 
         /**
            \brief push/pop scopes. 
@@ -140,13 +180,42 @@ namespace nla {
         /**
            \brief retrieve monomial corresponding to variable v from definition v := vs
         */
-        monomial const* var2monomial(lpvar v) const { unsigned idx = m_var2index.get(v, UINT_MAX); return idx == UINT_MAX ? nullptr : &m_monomials[idx]; }
+        monomial const& var2monomial(lpvar v) const { SASSERT(is_monomial_var(v)); return m_monomials[m_var2index[v]]; }
+
+        monomial const& operator[](lpvar v) const { return var2monomial(v); }
+
+        bool is_monomial_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; }
+
+        /**
+           \brief retrieve canonized monomial corresponding to variable v from definition v := vs
+        */
+        signed_vars const& var2canonical(lpvar v) const { return canonize(var2monomial(v)); }
+        
+        class canonical {
+            emonomials& m;
+        public:
+            canonical(emonomials& m): m(m) {}
+            signed_vars const& operator[](lpvar v) const { return m.var2canonical(v); }
+            signed_vars const& operator[](monomial const& mon) const { return m.var2canonical(mon.var()); }
+        };
+
+        canonical canonical;
         
         /**
            \brief obtain a canonized signed monomial
            corresponding to current equivalence class.
         */
-        signed_vars const& canonize(monomial const& m) const;
+        signed_vars const& canonize(monomial const& m) const { return m_canonized[m_var2index[m.var()]]; }
+
+        /**
+           \brief obtain the representative canonized monomial up to sign.
+        */
+        signed_vars const& rep(signed_vars const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
+
+        /**
+           \brief the original sign is defined as a sign of the equivalence class representative.
+        */
+        rational orig_sign(signed_vars const& sv) const { return rep(sv).rsign(); }           
 
         /**
            \brief determine if m1 divides m2 over the canonization obtained from merged variables.
@@ -192,7 +261,6 @@ namespace nla {
 
         use_list get_use_list(lpvar v) const { return use_list(*this, v); }
 
-
         /**
            \brief retrieve monomials m' where m is a proper factor of modulo current equalities.
         */
@@ -222,7 +290,49 @@ namespace nla {
         };
 
         factors_of get_factors_of(monomial const& m) const { inc_visited(); return factors_of(*this, m); }
-        
+        factors_of get_factors_of(lpvar v) const { return get_factors_of(var2monomial(v)); }
+       
+        signed_vars const* find_canonical(svector<lpvar> const& vars) const;
+
+        /**
+           \brief iterator over sign equivalent monomials.
+           These are monomials that are equivalent modulo m_var_eqs amd modulo signs.
+        */
+        class sign_equiv_monomials_it {
+            emonomials const& m;
+            unsigned m_index;
+            bool     m_touched;
+        public:
+            sign_equiv_monomials_it(emonomials const& m, unsigned idx, bool at_end): m(m), m_index(idx), m_touched(at_end) {}
+            monomial const& operator*() { return m.m_monomials[m_index]; }
+            sign_equiv_monomials_it& operator++() { 
+                m_touched = true; 
+                m_index = m.m_canonized[m_index].m_next; 
+                return *this; 
+            }
+            sign_equiv_monomials_it operator++(int) { sign_equiv_monomials_it tmp = *this; ++*this; return tmp; }
+            bool operator==(sign_equiv_monomials_it const& other) const { 
+                return m_index == other.m_index && m_touched == other.m_touched; 
+            }
+            bool operator!=(sign_equiv_monomials_it const& other) const { 
+                return m_index != other.m_index || m_touched != other.m_touched; 
+            }
+        };
+
+        class sign_equiv_monomials {
+            emonomials& em;
+            monomial const& m;
+            unsigned index() const { return em.m_var2index[m.var()]; }
+        public:
+            sign_equiv_monomials(emonomials & em, monomial const& m): em(em), m(m) {}
+            sign_equiv_monomials_it begin() { return sign_equiv_monomials_it(em, index(), false); }
+            sign_equiv_monomials_it end() { return sign_equiv_monomials_it(em, index(), true); }
+        };
+
+        sign_equiv_monomials enum_sign_equiv_monomials(monomial const& m) { return sign_equiv_monomials(*this, m); }
+        sign_equiv_monomials enum_sign_equiv_monomials(lpvar v) { return enum_sign_equiv_monomials((*this)[v]); }
+        sign_equiv_monomials enum_sign_equiv_monomials(signed_vars const& sv) { return enum_sign_equiv_monomials(sv.var()); }
+
         /**
            \brief display state of emonomials
         */
diff --git a/src/util/lp/factorization.cpp b/src/util/lp/factorization.cpp
index dddc2fa1b..da30c6cf3 100644
--- a/src/util/lp/factorization.cpp
+++ b/src/util/lp/factorization.cpp
@@ -24,26 +24,26 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
     std::sort(j_vars.begin(), j_vars.end());
 
     if (k_vars.size() == 1) {
-        k.index() = k_vars[0];
+        k.var() = k_vars[0];
         k.type() = factor_type::VAR;
     } else {
         unsigned i;
         if (!m_ff->find_rm_monomial_of_vars(k_vars, i)) {
             return false;
         }
-        k.index() = i;
+        k.var() = i;
         k.type() = factor_type::RM;
     }
 
     if (j_vars.size() == 1) {
-        j.index() = j_vars[0];
+        j.var() = j_vars[0];
         j.type() = factor_type::VAR;
     } else {
         unsigned i;
         if (!m_ff->find_rm_monomial_of_vars(j_vars, i)) {
             return false;
         }
-        j.index() = i;
+        j.var() = i;
         j.type() = factor_type::RM;
     }
     return true;
diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h
index 698bb90bc..56808824e 100644
--- a/src/util/lp/factorization.h
+++ b/src/util/lp/factorization.h
@@ -30,22 +30,22 @@ typedef unsigned lpvar;
 enum class factor_type { VAR, RM }; // RM stands for rooted monomial 
 
 class factor {
-    unsigned     m_index;
+    unsigned     m_var;
     factor_type  m_type;
 public:
     factor() {}
     explicit factor(unsigned j) : factor(j, factor_type::VAR) {}
-    factor(unsigned i, factor_type t) : m_index(i), m_type(t) {}
-    unsigned index() const { return m_index; }
-    unsigned& index() { return m_index; }
+    factor(unsigned i, factor_type t) : m_var(i), m_type(t) {}
+    unsigned var() const { return m_var; }
+    unsigned& var() { return m_var; }
     factor_type type() const { return m_type; }
     factor_type& type() { return m_type; }
     bool is_var() const { return m_type == factor_type::VAR; }
     bool operator==(factor const& other) const {
-        return m_index == other.index() && m_type == other.type();
+        return m_var == other.var() && m_type == other.type();
     }
     bool operator!=(factor const& other) const {
-        return m_index != other.index() || m_type != other.type();
+        return m_var != other.var() || m_type != other.type();
     }
 };
 
diff --git a/src/util/lp/factorization_factory_imp.cpp b/src/util/lp/factorization_factory_imp.cpp
index 98a75137a..d8ef706df 100644
--- a/src/util/lp/factorization_factory_imp.cpp
+++ b/src/util/lp/factorization_factory_imp.cpp
@@ -21,12 +21,12 @@
 #include "util/lp/nla_core.h"
 namespace nla {
         
-factorization_factory_imp::factorization_factory_imp(const rooted_mon& rm, const core& s) :
-        factorization_factory(rm.m_vars, &s.m_monomials[rm.orig_index()]),
-        m_core(s), m_mon(& s.m_monomials[rm.orig_index()]), m_rm(rm) { }
+factorization_factory_imp::factorization_factory_imp(const signed_vars& rm, const core& s) :
+    factorization_factory(rm.vars(), &s.m_emons[rm.var()]),
+    m_core(s), m_mon(s.m_emons[rm.var()]), m_rm(rm) { }
         
 bool factorization_factory_imp::find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
-        return m_core.find_rm_monomial_of_vars(vars, i);
+    return m_core.find_rm_monomial_of_vars(vars, i);
 }
 const monomial* factorization_factory_imp::find_monomial_of_vars(const svector<lpvar>& vars) const {
     return m_core.find_monomial_of_vars(vars);
diff --git a/src/util/lp/factorization_factory_imp.h b/src/util/lp/factorization_factory_imp.h
index f6d1bcba2..81b6b0037 100644
--- a/src/util/lp/factorization_factory_imp.h
+++ b/src/util/lp/factorization_factory_imp.h
@@ -20,15 +20,16 @@
 #pragma once
 #include "util/lp/factorization.h"
 namespace nla {
-struct core;
-struct rooted_mon;
-struct factorization_factory_imp: factorization_factory {
-    const core&  m_core;
-    const monomial *m_mon;
-    const rooted_mon& m_rm;
+    class  core;
+    class signed_vars;
+
+    struct factorization_factory_imp: factorization_factory {
+        const core&  m_core;
+        const monomial & m_mon;
+        const signed_vars& m_rm;
         
-    factorization_factory_imp(const rooted_mon& rm, const core& s);
-    bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const;
-    const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
-};
+        factorization_factory_imp(const signed_vars& rm, const core& s);
+        bool find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const;
+        const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
+    };
 }
diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp
index 5bf0c7c2e..efd3253b2 100644
--- a/src/util/lp/nla_basics_lemmas.cpp
+++ b/src/util/lp/nla_basics_lemmas.cpp
@@ -23,12 +23,13 @@
 namespace nla {
 
 basics::basics(core * c) : common(c) {}
+
 // Monomials m and n vars have the same values, up to "sign"
 // Generate a lemma if values of m.var() and n.var() are not the same up to sign
 bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign) {
-    if (vvr(m) == vvr(n) *sign)
+    if (vvr(m) == vvr(n) * sign)
         return false;
-    TRACE("nla_solver", tout << "sign contradiction:\nm = "; c().print_monomial_with_vars(m, tout); tout << "n= "; c().print_monomial_with_vars(n, tout); tout << "sign: " << sign << "\n";);
+    TRACE("nla_solver", tout << "sign contradiction:\nm = " << m << "n= " << n << "sign: " << sign << "\n";);
     generate_sign_lemma(m, n, sign);
     return true;
 }
@@ -40,17 +41,18 @@ void basics::generate_zero_lemmas(const monomial& m) {
     lpvar zero_j = find_best_zero(m, fixed_zeros);
     SASSERT(is_set(zero_j));
     unsigned zero_power = 0;
-    for (unsigned j : m){
+    for (lpvar j : m){
         if (j == zero_j) {
             zero_power++;
             continue;
         }
         get_non_strict_sign(j, sign);
-        if(sign == 0)
+        if (sign == 0)
             break;
     }
-    if (sign && is_even(zero_power))
+    if (sign && is_even(zero_power)) {
         sign = 0;
+    }
     TRACE("nla_solver_details", tout << "zero_j = " << zero_j << ", sign = " << sign << "\n";);
     if (sign == 0) { // have to generate a non-convex lemma
         add_trival_zero_lemma(zero_j, m);
@@ -98,10 +100,10 @@ void basics::basic_sign_lemma_model_based_one_mon(const monomial& m, int product
 }
     
 bool basics::basic_sign_lemma_model_based() {
-    unsigned i = c().random() % c().m_to_refine.size();
-    unsigned ii = i;
-    do {
-        const monomial& m = c().m_monomials[c().m_to_refine[i]];
+    unsigned start = c().random();
+    unsigned sz = c().m_to_refine.size();
+    for (unsigned i = sz; i-- > 0; ) {
+        monomial const& m = c().m_emons[c().m_to_refine[(start + i) % sz]];
         int mon_sign = nla::rat_sign(vvr(m));
         int product_sign = c().rat_sign(m);
         if (mon_sign != product_sign) {
@@ -109,47 +111,26 @@ bool basics::basic_sign_lemma_model_based() {
             if (c().done())
                 return true;
         }
-        i++;
-        if (i == c().m_to_refine.size())
-            i = 0;
-    } while (i != ii);
+    }
     return c().m_lemma_vec->size() > 0;
 }
 
     
-bool basics::basic_sign_lemma_on_mon(unsigned i, std::unordered_set<unsigned> & explored){
-    const monomial& m = c().m_monomials[i];
-    TRACE("nla_solver_details", tout << "i = " << i << ", mon = "; c().print_monomial_with_vars(m, tout););
-    const index_with_sign&  rm_i_s = c().m_rm_table.get_rooted_mon(i);
-    unsigned k = rm_i_s.index();
-    if (!try_insert(k, explored))
+bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set<unsigned> & explored){
+    if (!try_insert(v, explored)) {
         return false;
-
-    const auto& mons_to_explore = c().m_rm_table.rms()[k].m_mons;
-    TRACE("nla_solver", tout << "rm = "; c().print_rooted_monomial_with_vars(c().m_rm_table.rms()[k], tout) << "\n";);
-        
-    for (index_with_sign i_s : mons_to_explore) {
-        TRACE("nla_solver", tout << "i_s = (" << i_s.index() << "," << i_s.sign() << ")\n";
-              c().print_monomial_with_vars(c().m_monomials[i_s.index()], tout << "m = ") << "\n";
-              {
-                  for (lpvar j : c().m_monomials[i_s.index()] ) {
-                      lpvar rj = c().m_evars.find(j).var();
-                      if (j == rj)
-                          tout << "rj = j ="  << j << "\n";
-                      else {
-                          lp::explanation e;
-                          c().m_evars.explain(j, e);
-                          tout << "j = " << j << ", e = "; c().print_explanation(e, tout) << "\n";
-                      }
-                  }
-              }
-              );
-        unsigned n = i_s.index();
-        if (n == i) continue;
-        if (basic_sign_lemma_on_two_monomials(m, c().m_monomials[n], rm_i_s.sign()*i_s.sign()))
-            if(done())
-                return true;
     }
+
+    const monomial& m_v = c().m_emons[v];
+    signed_vars const& sv_v = c().m_emons.canonical[v];
+    TRACE("nla_solver_details", tout << "mon = " << m_v;);
+
+    for (auto const& m_w : c().m_emons.enum_sign_equiv_monomials(v)) {
+        signed_vars const& sv_w = c().m_emons.canonical[m_w];
+        if (m_v.var() != m_w.var() && basic_sign_lemma_on_two_monomials(m_v, m_w, sv_v.rsign() * sv_w.rsign()) && done()) 
+            return true;
+    }
+
     TRACE("nla_solver_details", tout << "return false\n";);
     return false;
 }
@@ -163,7 +144,7 @@ bool basics::basic_sign_lemma(bool derived) {
         return basic_sign_lemma_model_based();
 
     std::unordered_set<unsigned> explored;
-    for (unsigned i : c().m_to_refine){
+    for (lpvar i : c().m_to_refine){
         if (basic_sign_lemma_on_mon(i, explored))
             return true;
     }
@@ -241,7 +222,10 @@ void basics::negate_strict_sign(lpvar j) {
 
 // here we use the fact
 // xy = 0 -> x = 0 or y = 0
-bool basics::basic_lemma_for_mon_zero(const rooted_mon& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_zero(const signed_vars& rm, const factorization& f) {
+    NOT_IMPLEMENTED_YET();
+    return true;
+#if 0
     TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
     add_empty_lemma();
     c().explain_fixed_var(var(rm));
@@ -253,6 +237,7 @@ bool basics::basic_lemma_for_mon_zero(const rooted_mon& rm, const factorization&
     explain(rm);
     TRACE("nla_solver", c().print_lemma(tout););
     return true;
+#endif
 }
 // use basic multiplication properties to create a lemma
 bool basics::basic_lemma(bool derived) {
@@ -261,31 +246,27 @@ bool basics::basic_lemma(bool derived) {
     if (derived)
         return false;
     c().init_rm_to_refine();
-    const auto& rm_ref = c().m_rm_table.to_refine();
+    const auto& rm_ref = c().m_to_refine;
     TRACE("nla_solver", tout << "rm_ref = "; print_vector(rm_ref, tout););
-    unsigned start = c().random() % rm_ref.size();
-    unsigned i = start;
-    do {
-        const rooted_mon& r = c().m_rm_table.rms()[rm_ref[i]];
-        SASSERT (!c().check_monomial(c().m_monomials[r.orig_index()]));
+    unsigned start = c().random();
+    for (unsigned j = rm_ref.size(); j-- > 0; ) {
+        const signed_vars& r = c().m_emons.canonical[(j + start) % rm_ref.size()];
+        SASSERT (!c().check_monomial(c().m_emons[r.var()]));
         basic_lemma_for_mon(r, derived);
-        if (++i == rm_ref.size()) {
-            i = 0;
-        }
-    } while(i != start && !done());
+    } 
         
     return false;
 }
 // Use basic multiplication properties to create a lemma
 // for the given monomial.
 // "derived" means derived from constraints - the alternative is model based
-void basics::basic_lemma_for_mon(const rooted_mon& rm, bool derived) {
+void basics::basic_lemma_for_mon(const signed_vars& rm, bool derived) {
     if (derived)
         basic_lemma_for_mon_derived(rm);
     else
         basic_lemma_for_mon_model_based(rm);
 }
-bool basics::basic_lemma_for_mon_derived(const rooted_mon& rm) {
+bool basics::basic_lemma_for_mon_derived(const signed_vars& rm) {
     if (c().var_is_fixed_to_zero(var(rm))) {
         for (auto factorization : factorization_factory_imp(rm, c())) {
             if (factorization.is_empty())
@@ -311,7 +292,7 @@ bool basics::basic_lemma_for_mon_derived(const rooted_mon& rm) {
     return false;
 }
 // x = 0 or y = 0 -> xy = 0
-bool basics::basic_lemma_for_mon_non_zero_derived(const rooted_mon& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_non_zero_derived(const signed_vars& rm, const factorization& f) {
     TRACE("nla_solver", c().trace_print_monomial_and_factorization(rm, f, tout););
     if (! c().var_is_separated_from_zero(var(rm)))
         return false; 
@@ -335,10 +316,10 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const rooted_mon& rm, const fa
 }
 // use the fact that
 // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
-bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const rooted_mon& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const signed_vars& rm, const factorization& f) {
     TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout););
 
-    lpvar mon_var =  c().m_monomials[rm.orig_index()].var();
+    lpvar mon_var =  c().m_emons[rm.var()].var();
     TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
         
     const auto & mv = vvr(mon_var);
@@ -395,9 +376,9 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const rooted
 }
 // use the fact
 // 1 * 1 ... * 1 * x * 1 ... * 1 = x
-bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const rooted_mon& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const signed_vars& rm, const factorization& f) {
     return false;
-    rational sign = rm.orig().m_sign;
+    rational sign = c().m_emons.orig_sign(rm);
     lpvar not_one = -1;
 
     TRACE("nla_solver", tout << "f = ";  c().print_factorization(f, tout););
@@ -432,17 +413,17 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const
     }
 
     if (not_one == static_cast<lpvar>(-1)) {
-        c().mk_ineq( c().m_monomials[rm.orig_index()].var(), llc::EQ, sign);
+        c().mk_ineq( c().m_emons[rm.var()].var(), llc::EQ, sign);
     } else {
-        c().mk_ineq( c().m_monomials[rm.orig_index()].var(), -sign, not_one, llc::EQ);
+        c().mk_ineq( c().m_emons[rm.var()].var(), -sign, not_one, llc::EQ);
     }
     TRACE("nla_solver",
-          tout << "rm = ";  c().print_rooted_monomial_with_vars(rm, tout);
-           c().print_lemma(tout););
+          tout << "rm = " << rm;
+          c().print_lemma(tout););
     return true;
 }
 
-bool basics::basic_lemma_for_mon_neutral_derived(const rooted_mon& rm, const factorization& factorization) {
+bool basics::basic_lemma_for_mon_neutral_derived(const signed_vars& rm, const factorization& factorization) {
     return
         basic_lemma_for_mon_neutral_monomial_to_factor_derived(rm, factorization) || 
         basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(rm, factorization);
@@ -450,7 +431,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const rooted_mon& rm, const fac
 }
 
 // x != 0 or y = 0 => |xy| >= |y|
-void basics::proportion_lemma_model_based(const rooted_mon& rm, const factorization& factorization) {
+void basics::proportion_lemma_model_based(const signed_vars& rm, const factorization& factorization) {
     rational rmv = abs(vvr(rm));
     if (rmv.is_zero()) {
         SASSERT(c().has_zero_factor(factorization));
@@ -466,7 +447,7 @@ void basics::proportion_lemma_model_based(const rooted_mon& rm, const factorizat
     }
 }
 // x != 0 or y = 0 => |xy| >= |y|
-bool basics::proportion_lemma_derived(const rooted_mon& rm, const factorization& factorization) {
+bool basics::proportion_lemma_derived(const signed_vars& rm, const factorization& factorization) {
     return false;
     rational rmv = abs(vvr(rm));
     if (rmv.is_zero()) {
@@ -507,11 +488,11 @@ void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
     
 // none of the factors is zero and the product is not zero
 // -> |fc[factor_index]| <= |rm|
-void basics::generate_pl(const rooted_mon& rm, const factorization& fc, int factor_index) {
+void basics::generate_pl(const signed_vars& rm, const factorization& fc, int factor_index) {
     TRACE("nla_solver", tout << "factor_index = " << factor_index << ", rm = ";
-          c().print_rooted_monomial_with_vars(rm, tout);
+          tout << rm;
           tout << "fc = "; c().print_factorization(fc, tout);
-          tout << "orig mon = "; c().print_monomial(c().m_monomials[rm.orig_index()], tout););
+          tout << "orig mon = "; c().print_monomial(c().m_emons[rm.var()], tout););
     if (fc.is_mon()) {
         generate_pl_on_mon(*fc.mon(), factor_index);
         return;
@@ -541,7 +522,7 @@ void basics::generate_pl(const rooted_mon& rm, const factorization& fc, int fact
     TRACE("nla_solver", c().print_lemma(tout); );
 }   
 // here we use the fact xy = 0 -> x = 0 or y = 0
-void basics::basic_lemma_for_mon_zero_model_based(const rooted_mon& rm, const factorization& f) {        
+void basics::basic_lemma_for_mon_zero_model_based(const signed_vars& rm, const factorization& f) {        
     TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout););
     SASSERT(vvr(rm).is_zero()&& ! c().rm_check(rm));
     add_empty_lemma();
@@ -562,8 +543,8 @@ void basics::basic_lemma_for_mon_zero_model_based(const rooted_mon& rm, const fa
     TRACE("nla_solver", c().print_lemma(tout););
 }
 
-void basics::basic_lemma_for_mon_model_based(const rooted_mon& rm) {
-    TRACE("nla_solver_bl", tout << "rm = "; c().print_rooted_monomial(rm, tout););
+void basics::basic_lemma_for_mon_model_based(const signed_vars& rm) {
+    TRACE("nla_solver_bl", tout << "rm = " << rm;);
     if (vvr(rm).is_zero()) {
         for (auto factorization : factorization_factory_imp(rm, c())) {
             if (factorization.is_empty())
@@ -682,10 +663,10 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
 
 // use the fact that
 // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
-bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const rooted_mon& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const signed_vars& rm, const factorization& f) {
     TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
 
-    lpvar mon_var = c().m_monomials[rm.orig_index()].var();
+    lpvar mon_var = c().m_emons[rm.var()].var();
     TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";);
         
     const auto & mv = vvr(mon_var);
@@ -740,7 +721,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const ro
     return true;
 }
 
-void basics::basic_lemma_for_mon_neutral_model_based(const rooted_mon& rm, const factorization& f) {
+void basics::basic_lemma_for_mon_neutral_model_based(const signed_vars& rm, const factorization& f) {
     if (f.is_mon()) {
         basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(*f.mon());
         basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(*f.mon());
@@ -752,8 +733,8 @@ void basics::basic_lemma_for_mon_neutral_model_based(const rooted_mon& rm, const
 }
 // use the fact
 // 1 * 1 ... * 1 * x * 1 ... * 1 = x
-bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const rooted_mon& rm, const factorization& f) {
-    rational sign = rm.orig_sign();
+bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const signed_vars& rm, const factorization& f) {
+    rational sign = c().m_emons.orig_sign(rm);
     TRACE("nla_solver_bl", tout << "f = "; c().print_factorization(f, tout); tout << ", sign = " << sign << '\n'; );
     lpvar not_one = -1;
     for (auto j : f){
@@ -801,15 +782,15 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
     }
 
     if (not_one == static_cast<lpvar>(-1)) {
-        c().mk_ineq(c().m_monomials[rm.orig_index()].var(), llc::EQ, sign);
+        c().mk_ineq(rm.var(), llc::EQ, sign);
     } else {
-        c().mk_ineq(c().m_monomials[rm.orig_index()].var(), -sign, not_one, llc::EQ);
+        c().mk_ineq(rm.var(), -sign, not_one, llc::EQ);
     }
     explain(rm);
     explain(f);
     TRACE("nla_solver",
           c().print_lemma(tout);
-          tout << "rm = "; c().print_rooted_monomial_with_vars(rm, tout);
+          tout << "rm = " << rm;
           );
     return true;
 }
@@ -833,7 +814,7 @@ void basics::basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f)
 }
 
 // x = 0 or y = 0 -> xy = 0
-void basics::basic_lemma_for_mon_non_zero_model_based(const rooted_mon& rm, const factorization& f) {
+void basics::basic_lemma_for_mon_non_zero_model_based(const signed_vars& rm, const factorization& f) {
     TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
     if (f.is_mon())
         basic_lemma_for_mon_non_zero_model_based_mf(f);
diff --git a/src/util/lp/nla_basics_lemmas.h b/src/util/lp/nla_basics_lemmas.h
index ec31863e6..62f1ff9d9 100644
--- a/src/util/lp/nla_basics_lemmas.h
+++ b/src/util/lp/nla_basics_lemmas.h
@@ -25,7 +25,7 @@
 
 
 namespace nla {
-struct core;
+class core;
 struct basics: common {
     basics(core *core);
     bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign);
@@ -40,47 +40,47 @@ struct basics: common {
      -ab = a(-b)
     */
     bool basic_sign_lemma(bool derived);
-    bool basic_lemma_for_mon_zero(const rooted_mon& rm, const factorization& f);
+    bool basic_lemma_for_mon_zero(const signed_vars& rm, const factorization& f);
 
-    void basic_lemma_for_mon_zero_model_based(const rooted_mon& rm, const factorization& f);
+    void basic_lemma_for_mon_zero_model_based(const signed_vars& rm, const factorization& f);
 
-    void basic_lemma_for_mon_non_zero_model_based(const rooted_mon& rm, const factorization& f);
+    void basic_lemma_for_mon_non_zero_model_based(const signed_vars& rm, const factorization& f);
     // x = 0 or y = 0 -> xy = 0
-    void basic_lemma_for_mon_non_zero_model_based_rm(const rooted_mon& rm, const factorization& f);
+    void basic_lemma_for_mon_non_zero_model_based_rm(const signed_vars& rm, const factorization& f);
 
     void basic_lemma_for_mon_non_zero_model_based_mf(const factorization& f);
     // x = 0 or y = 0 -> xy = 0
-    bool basic_lemma_for_mon_non_zero_derived(const rooted_mon& rm, const factorization& f);
+    bool basic_lemma_for_mon_non_zero_derived(const signed_vars& rm, const factorization& f);
 
     // use the fact that
     // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
-    bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const rooted_mon& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const signed_vars& rm, const factorization& f);
     // use the fact that
     // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 
     bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const monomial& m);
-    bool basic_lemma_for_mon_neutral_monomial_to_factor_derived(const rooted_mon& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_monomial_to_factor_derived(const signed_vars& rm, const factorization& f);
 
     // use the fact
     // 1 * 1 ... * 1 * x * 1 ... * 1 = x
-    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const rooted_mon& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const signed_vars& rm, const factorization& f);
     // use the fact
     // 1 * 1 ... * 1 * x * 1 ... * 1 = x
     bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm(const monomial& m);
     // use the fact
     // 1 * 1 ... * 1 * x * 1 ... * 1 = x
-    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const rooted_mon& rm, const factorization& f);
-    void basic_lemma_for_mon_neutral_model_based(const rooted_mon& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const signed_vars& rm, const factorization& f);
+    void basic_lemma_for_mon_neutral_model_based(const signed_vars& rm, const factorization& f);
     
-    bool basic_lemma_for_mon_neutral_derived(const rooted_mon& rm, const factorization& factorization);
+    bool basic_lemma_for_mon_neutral_derived(const signed_vars& rm, const factorization& factorization);
 
-    void basic_lemma_for_mon_model_based(const rooted_mon& rm);
+    void basic_lemma_for_mon_model_based(const signed_vars& rm);
 
-    bool basic_lemma_for_mon_derived(const rooted_mon& rm);
+    bool basic_lemma_for_mon_derived(const signed_vars& rm);
     
     // Use basic multiplication properties to create a lemma
     // for the given monomial.
     // "derived" means derived from constraints - the alternative is model based
-    void basic_lemma_for_mon(const rooted_mon& rm, bool derived);
+    void basic_lemma_for_mon(const signed_vars& rm, bool derived);
     // use basic multiplication properties to create a lemma
     bool basic_lemma(bool derived);
     void generate_sign_lemma(const monomial& m, const monomial& n, const rational& sign);
@@ -94,14 +94,14 @@ struct basics: common {
     void add_fixed_zero_lemma(const monomial& m, lpvar j);
     void negate_strict_sign(lpvar j);
     // x != 0 or y = 0 => |xy| >= |y|
-    void proportion_lemma_model_based(const rooted_mon& rm, const factorization& factorization);
+    void proportion_lemma_model_based(const signed_vars& rm, const factorization& factorization);
     // x != 0 or y = 0 => |xy| >= |y|
-    bool proportion_lemma_derived(const rooted_mon& rm, const factorization& factorization);
+    bool proportion_lemma_derived(const signed_vars& rm, const factorization& factorization);
     // if there are no zero factors then |m| >= |m[factor_index]|
     void generate_pl_on_mon(const monomial& m, unsigned factor_index);
     
     // none of the factors is zero and the product is not zero
     // -> |fc[factor_index]| <= |rm|
-    void generate_pl(const rooted_mon& rm, const factorization& fc, int factor_index);   
+    void generate_pl(const signed_vars& rm, const factorization& fc, int factor_index);   
 };
 }
diff --git a/src/util/lp/nla_common.cpp b/src/util/lp/nla_common.cpp
index aba5f810e..8de119271 100644
--- a/src/util/lp/nla_common.cpp
+++ b/src/util/lp/nla_common.cpp
@@ -21,31 +21,31 @@
 #include "util/lp/nla_core.h"
 
 namespace nla {
-bool common::done() const { return m_core->done(); }
+bool common::done() const { return c().done(); }
 
 template <typename T> void common::explain(const T& t) {
     c().explain(t, c().current_expl());
 }
 template void common::explain<monomial>(const monomial& t);
 template void common::explain<factor>(const factor& t);
-template void common::explain<rooted_mon>(const rooted_mon& t);
+template void common::explain<signed_vars>(const signed_vars& t);
 template void common::explain<factorization>(const factorization& t);
 
 void common::explain(lpvar j) { c().explain(j, c().current_expl()); }
 
-template <typename T> rational common::vvr(T const& t) const { return m_core->vvr(t); }
+template <typename T> rational common::vvr(T const& t) const { return c().vvr(t); }
 template rational common::vvr<monomial>(monomial const& t) const;
-template rational common::vvr<rooted_mon>(rooted_mon const& t) const;
+template rational common::vvr<signed_vars>(signed_vars const& t) const;
 template rational common::vvr<factor>(factor const& t) const;
-rational common::vvr(lpvar t) const { return m_core->vvr(t); }
-template <typename T> lpvar common::var(T const& t) const { return m_core->var(t); }
+rational common::vvr(lpvar t) const { return c().vvr(t); }
+template <typename T> lpvar common::var(T const& t) const { return c().var(t); }
 template lpvar common::var<factor>(factor const& t) const;
-template lpvar common::var<rooted_mon>(rooted_mon const& t) const;
+template lpvar common::var<signed_vars>(signed_vars const& t) const;
 void common::add_empty_lemma() { c().add_empty_lemma(); }
 template <typename T> rational common::canonize_sign(const T& t) const {
     return c().canonize_sign(t);
 }
-template rational common::canonize_sign<rooted_mon>(const rooted_mon& t) const;
+template rational common::canonize_sign<signed_vars>(const signed_vars& t) const;
 template rational common::canonize_sign<factor>(const factor& t) const;
 rational common::canonize_sign(lpvar j) const {
     return c().canonize_sign_of_var(j);
@@ -99,18 +99,19 @@ std::ostream& common::print_product(const T & m, std::ostream& out) const {
 template 
 std::ostream& common::print_product<monomial>(const monomial & m, std::ostream& out) const;
 
-template std::ostream& common::print_product<rooted_mon>(const rooted_mon & m, std::ostream& out) const;
+template std::ostream& common::print_product<signed_vars>(const signed_vars & m, std::ostream& out) const;
 
 
 std::ostream& common::print_monomial(const monomial & m, std::ostream& out) const {
     return c().print_monomial(m, out);
 }
-std::ostream& common::print_rooted_monomial(const rooted_mon& rm, std::ostream& out) const {
-    return c().print_rooted_monomial(rm, out);
-}
-std::ostream& common::print_rooted_monomial_with_vars(const rooted_mon& rm, std::ostream& out) const {
-        return c().print_rooted_monomial_with_vars(rm, out);
-}
+
+//std::ostream& common::print_rooted_monomial(const signed_vars& rm, std::ostream& out) const {
+//    return c().print_rooted_monomial(rm, out);
+//}
+//std::ostream& common::print_rooted_monomial_with_vars(const signed_vars& rm, std::ostream& out) const {
+//        return c().print_rooted_monomial_with_vars(rm, out);
+//}
 std::ostream& common::print_factor(const factor & f, std::ostream& out) const {
     return c().print_factor(f, out);
 }
diff --git a/src/util/lp/nla_common.h b/src/util/lp/nla_common.h
index b168ebc96..00665fe67 100644
--- a/src/util/lp/nla_common.h
+++ b/src/util/lp/nla_common.h
@@ -22,9 +22,11 @@
 #include "util/lp/nla_defs.h"
 #include "util/lp/lar_term.h"
 #include "util/lp/monomial.h"
+#include "util/lp/emonomials.h"
 #include "util/lp/factorization.h"
-#include "util/lp/rooted_mons.h"
 namespace nla {
+
+
 inline llc negate(llc cmp) {
     switch(cmp) {
     case llc::LE: return llc::GT;
@@ -38,7 +40,7 @@ inline llc negate(llc cmp) {
     return cmp; // not reachable
 }
 
-struct core;
+class core;
 struct common {
     core* m_core;
     common(core* c): m_core(c) {}
@@ -82,8 +84,8 @@ struct common {
     std::ostream& print_var(lpvar, std::ostream& out) const;
     
     std::ostream& print_monomial(const monomial & m, std::ostream& out) const;
-    std::ostream& print_rooted_monomial(const rooted_mon &, std::ostream& out) const;
-    std::ostream& print_rooted_monomial_with_vars(const rooted_mon&, std::ostream& out) const;
+    std::ostream& print_rooted_monomial(const signed_vars &, std::ostream& out) const;
+    std::ostream& print_rooted_monomial_with_vars(const signed_vars&, std::ostream& out) const;
     bool check_monomial(const monomial&) const;
     unsigned random();
 };
diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index 27da6dd52..717ab2a48 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -79,75 +79,46 @@ bool core::lemma_holds(const lemma& l) const {
     
 svector<lpvar> core::sorted_vars(const factor& f) const {
     if (f.is_var()) {
-        svector<lpvar> r; r.push_back(f.index());
+        svector<lpvar> r; r.push_back(f.var());
         return r;
     }
     TRACE("nla_solver", tout << "nv";);
-    return m_rm_table.rms()[f.index()].vars();
+    return m_emons.canonical[f.var()].vars();
 }
 
 // the value of the factor is equal to the value of the variable multiplied
 // by the canonize_sign
 rational core::canonize_sign(const factor& f) const {
     return f.is_var()?
-        canonize_sign_of_var(f.index()) : m_rm_table.rms()[f.index()].orig_sign();
+        canonize_sign_of_var(f.var()) : m_emons.canonical[f.var()].rsign();
 }
 
 rational core::canonize_sign_of_var(lpvar j) const {
     return m_evars.find(j).rsign();        
 }
     
-// the value of the rooted monomias is equal to the value of the variable multiplied
-// by the canonize_sign
-rational core::canonize_sign(const rooted_mon& m) const {
-    return m.orig().sign();
+rational core::canonize_sign(const signed_vars& m) const {
+    NOT_IMPLEMENTED_YET();
+    return rational::one();
 }
+
     
 // returns the monomial index
-unsigned core::add(lpvar v, unsigned sz, lpvar const* vs) {
-    m_monomials.push_back(monomial(v, sz, vs));
-    TRACE("nla_solver", print_monomial(m_monomials.back(), tout););
-    const auto & m = m_monomials.back();
-    SASSERT(m_mkeys.find(m.vars()) == m_mkeys.end());
-    return m_mkeys[m.vars()] = m_monomials.size() - 1;
+void core::add(lpvar v, unsigned sz, lpvar const* vs) {
+    m_emons.add(v, sz, vs);
 }
     
 void core::push() {
     TRACE("nla_solver",);
-    m_monomials_counts.push_back(m_monomials.size());
-    m_evars.push();
+    m_emons.push();
 }
 
-void core::deregister_monomial_from_rooted_monomials (const monomial & m, unsigned i){
-    rational sign = rational(1);
-    svector<lpvar> vars = reduce_monomial_to_rooted(m.vars(), sign);
-    NOT_IMPLEMENTED_YET();
-}
-
-void core::deregister_monomial_from_tables(const monomial & m, unsigned i){
-    TRACE("nla_solver", tout << "m = "; print_monomial(m, tout););
-    m_mkeys.erase(m.vars());
-    deregister_monomial_from_rooted_monomials(m, i);     
-}
      
 void core::pop(unsigned n) {
-    TRACE("nla_solver", tout << "n = " << n <<
-          " , m_monomials_counts.size() = " << m_monomials_counts.size() << ", m_monomials.size() = " << m_monomials.size() << "\n"; );
-    if (n == 0) return;
-    unsigned new_size = m_monomials_counts[m_monomials_counts.size() - n];
-    TRACE("nla_solver", tout << "new_size = " << new_size << "\n"; );
-        
-    for (unsigned i = m_monomials.size(); i-- > new_size; ){
-        deregister_monomial_from_tables(m_monomials[i], i);
-    }
-    m_monomials.shrink(new_size);
-    m_monomials_counts.shrink(m_monomials_counts.size() - n);
-    m_evars.pop(n);
+    TRACE("nla_solver", tout << "n = " << n << "\n";);
+    m_emons.pop(n);
 }
 
-rational core::mon_value_by_vars(unsigned i) const {
-    return product_value(m_monomials[i]);
-}
 template <typename T>
 rational core::product_value(const T & m) const {
     rational r(1);
@@ -168,16 +139,15 @@ void core::explain(const monomial& m, lp::explanation& exp) const {
         explain(j, exp);
 }
 
-void core::explain(const rooted_mon& rm, lp::explanation& exp) const {
-    auto & m = m_monomials[rm.orig_index()];
-    explain(m, exp);
+void core::explain(const signed_vars& rm, lp::explanation& exp) const {
+    explain(m_emons[rm.var()], exp);
 }
 
 void core::explain(const factor& f, lp::explanation& exp) const {
     if (f.type() == factor_type::VAR) {
-        explain(f.index(), exp);
+        explain(f.var(), exp);
     } else {
-        explain(m_monomials[m_rm_table.rms()[f.index()].orig_index()], exp);
+        explain(m_emons[f.var()], exp);
     }
 }
 
@@ -187,22 +157,23 @@ void core::explain(lpvar j, lp::explanation& exp) const {
 
 template <typename T>
 std::ostream& core::print_product(const T & m, std::ostream& out) const {
-    for (unsigned k = 0; k < m.size(); k++) {
-        out << "(" << m_lar_solver.get_variable_name(m[k]) << "=" << vvr(m[k]) << ")";
-        if (k + 1 < m.size()) out << "*";
+    bool first = true;
+    for (lpvar v : m) {
+        if (!first) out << "*"; else first = false;
+        out << "(" << m_lar_solver.get_variable_name(v) << "=" << vvr(v) << ")";
     }
     return out;
 }
 template std::ostream& core::print_product<monomial>(const monomial & m, std::ostream& out) const;
-template std::ostream& core::print_product<rooted_mon>(const rooted_mon & m, std::ostream& out) const;
+template std::ostream& core::print_product<signed_vars>(const signed_vars & m, std::ostream& out) const;
 
 std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
     if (f.is_var()) {
         out << "VAR,  ";
-        print_var(f.index(), out);
+        print_var(f.var(), out);
     } else {
         out << "PROD, ";
-        print_product(m_rm_table.rms()[f.index()].vars(), out);
+        print_product(m_emons.canonical[f.var()].vars(), out);
     }
     out << "\n";
     return out;
@@ -210,10 +181,10 @@ std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
 
 std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out) const {
     if (f.is_var()) {
-        print_var(f.index(), out);
+        print_var(f.var(), out);
     } else {
-        out << " RM = "; print_rooted_monomial_with_vars(m_rm_table.rms()[f.index()], out);
-        out << "\n orig mon = "; print_monomial_with_vars(m_monomials[m_rm_table.rms()[f.index()].orig_index()], out);
+        out << " RM = " << m_emons.canonical[f.var()];
+        out << "\n orig mon = " << m_emons[f.var()];
     }
     return out;
 }
@@ -241,11 +212,11 @@ std::ostream& core::print_bfc(const bfc& m, std::ostream& out) const {
 }
 
 std::ostream& core::print_monomial(unsigned i, std::ostream& out) const {
-    return print_monomial(m_monomials[i], out);
+    return print_monomial(m_emons[i], out);
 }
 
-std::ostream& core::print_monomial_with_vars(unsigned i, std::ostream& out) const {
-    return print_monomial_with_vars(m_monomials[i], out);
+std::ostream& core::print_monomial_with_vars(lpvar v, std::ostream& out) const {
+    return print_monomial_with_vars(m_emons[v], out);
 }
 
 template <typename T>
@@ -260,30 +231,12 @@ std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const
 
 std::ostream& core::print_monomial_with_vars(const monomial& m, std::ostream& out) const {
     out << "["; print_var(m.var(), out) << "]\n";
-    for(lpvar j: m)
+    for (lpvar j: m)
         print_var(j, out);
     out << ")\n";
     return out;
 }
 
-std::ostream& core::print_rooted_monomial(const rooted_mon& rm, std::ostream& out) const {
-    out << "vars = "; 
-    print_product(rm.vars(), out);
-    out << "\n orig = "; print_monomial(m_monomials[rm.orig_index()], out);
-    out << ", orig sign = " << rm.orig_sign() << "\n";
-    return out;
-}
-
-std::ostream& core::print_rooted_monomial_with_vars(const rooted_mon& rm, std::ostream& out) const {
-    out << "vars = "; 
-    print_product(rm.vars(), out);
-    out << "\n orig = "; print_monomial_with_vars(m_monomials[rm.orig_index()], out);
-    out << ", orig sign = " << rm.orig_sign() << "\n";
-    out << ", vvr(rm) = " << vvr(rm) << "\n";
-        
-    return out;
-}
-
 std::ostream& core::print_explanation(const lp::explanation& exp, std::ostream& out) const {
     out << "expl: ";
     for (auto &p : exp) {
@@ -400,13 +353,12 @@ bool core:: explain_ineq(const lp::lar_term& t, llc cmp, const rational& rs) {
             (rs.is_zero() && explain_by_equiv(t, exp));
         break;
     case llc::NE:
-        r = explain_lower_bound(t, rs + rational(1), exp) || explain_upper_bound(t, rs - rational(1), exp);
-            
-            
+        // TBD - NB: does this work for Reals?
+        r = explain_lower_bound(t, rs + rational(1), exp) || explain_upper_bound(t, rs - rational(1), exp);           
         break;
     default:
-        SASSERT(false);
-        r = false;
+        UNREACHABLE();
+        return false;
     }
     if (r) {
         current_expl().add(exp);
@@ -426,10 +378,10 @@ bool core:: explain_by_equiv(const lp::lar_term& t, lp::explanation& e) {
     bool sign;
     if (!is_octagon_term(t, sign, i, j))
         return false;
-    if (m_evars.find(signed_var(i,false)) != m_evars.find(signed_var(j, sign)))
+    if (m_evars.find(signed_var(i, false)) != m_evars.find(signed_var(j, sign)))
         return false;
             
-    m_evars.explain(signed_var(i,false), signed_var(j, sign), e);
+    m_evars.explain(signed_var(i, false), signed_var(j, sign), e);
     TRACE("nla_solver", tout << "explained :"; m_lar_solver.print_term(t, tout););
     return true;
             
@@ -437,13 +389,12 @@ bool core:: explain_by_equiv(const lp::lar_term& t, lp::explanation& e) {
     
 void core::mk_ineq(lp::lar_term& t, llc cmp, const rational& rs) {
     TRACE("nla_solver_details", m_lar_solver.print_term(t, tout << "t = "););
-    if (explain_ineq(t, cmp, rs)) {
-        return;
+    if (!explain_ineq(t, cmp, rs)) {
+        m_lar_solver.subs_term_columns(t);
+        current_lemma().push_back(ineq(cmp, t, rs));
+        CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";);
+        SASSERT(!ineq_holds(ineq(cmp, t, rs)));
     }
-    m_lar_solver.subs_term_columns(t);
-    current_lemma().push_back(ineq(cmp, t, rs));
-    CTRACE("nla_solver", ineq_holds(ineq(cmp, t, rs)), print_ineq(ineq(cmp, t, rs), tout) << "\n";);
-    SASSERT(!ineq_holds(ineq(cmp, t, rs)));
 }
 
 void core::mk_ineq(const rational& a, lpvar j, const rational& b, lpvar k, llc cmp, const rational& rs) {
@@ -781,9 +732,8 @@ std::ostream & core::print_ineq(const ineq & in, std::ostream & out) const {
 }
 
 std::ostream & core::print_var(lpvar j, std::ostream & out) const {
-    auto it = m_var_to_its_monomial.find(j);
-    if (it != m_var_to_its_monomial.end()) {
-        print_monomial(m_monomials[it->second], out);
+    if (m_emons.is_monomial_var(j)) {
+        print_monomial(m_emons[j], out);
         out << " = " << vvr(j);;
     }
         
@@ -792,7 +742,7 @@ std::ostream & core::print_var(lpvar j, std::ostream & out) const {
 }
 
 std::ostream & core::print_monomials(std::ostream & out) const {
-    for (auto &m : m_monomials) {
+    for (auto &m : m_emons) {
         print_monomial_with_vars(m, out);
     }
     return out;
@@ -835,23 +785,13 @@ std::ostream & core::print_factorization(const factorization& f, std::ostream& o
     
 bool core:: find_rm_monomial_of_vars(const svector<lpvar>& vars, unsigned & i) const {
     SASSERT(vars_are_roots(vars));
-    auto it = m_rm_table.vars_key_to_rm_index().find(vars);
-    if (it == m_rm_table.vars_key_to_rm_index().end()) {
-        return false;
-    }
-        
-    i = it->second;
-    TRACE("nla_solver",);
-        
-    SASSERT(lp::vectors_are_equal_(vars, m_rm_table.rms()[i].vars()));
-    return true;
+    signed_vars const* sv = m_emons.find_canonical(vars);
+    return sv && (i = sv->var(), true);
 }
 
 const monomial* core::find_monomial_of_vars(const svector<lpvar>& vars) const {
-    unsigned i;
-    if (!find_rm_monomial_of_vars(vars, i))
-        return nullptr;
-    return &m_monomials[m_rm_table.rms()[i].orig_index()];
+    signed_vars const* sv = m_emons.find_canonical(vars);
+    return sv ? &m_emons[sv->var()] : nullptr;
 }
 
 
@@ -873,8 +813,8 @@ void core::explain_separation_from_zero(lpvar j) {
         explain_existing_upper_bound(j);
 }
 
-int core::get_derived_sign(const rooted_mon& rm, const factorization& f) const {
-    rational sign = rm.orig_sign(); // this is the flip sign of the variable var(rm)
+int core::get_derived_sign(const signed_vars& rm, const factorization& f) const {
+    rational sign = rm.rsign(); // this is the flip sign of the variable var(rm)
     SASSERT(!sign.is_zero());
     for (const factor& fc: f) {
         lpvar j = var(fc);
@@ -885,12 +825,12 @@ int core::get_derived_sign(const rooted_mon& rm, const factorization& f) const {
     }
     return nla::rat_sign(sign);
 }
-void core::trace_print_monomial_and_factorization(const rooted_mon& rm, const factorization& f, std::ostream& out) const {
+void core::trace_print_monomial_and_factorization(const signed_vars& rm, const factorization& f, std::ostream& out) const {
     out << "rooted vars: ";
-    print_product(rm.m_vars, out);
+    print_product(rm.vars(), out);
     out << "\n";
         
-    print_monomial(rm.orig_index(), out << "mon:  ") << "\n";
+    print_monomial(rm.var(), out << "mon:  ") << "\n";
     out << "value: " << vvr(rm) << "\n";
     print_factorization(f, out << "fact: ") << "\n";
 }
@@ -1338,13 +1278,6 @@ bool core:: mon_has_zero(const T& product) const {
 
 template bool core::mon_has_zero<monomial>(const monomial& product) const;
 
-void core::init_rm_to_refine() {
-    if (!m_rm_table.to_refine().empty())
-        return;
-    std::unordered_set<unsigned> ref;
-    ref.insert(m_to_refine.begin(), m_to_refine.end());
-    m_rm_table.init_to_refine(ref);
-}
 
 lp::lp_settings& core::settings() {
     return m_lar_solver.settings();
@@ -1352,53 +1285,6 @@ lp::lp_settings& core::settings() {
     
 unsigned core::random() { return settings().random_next(); }
     
-// use basic multiplication properties to create a lemma
-bool core:: basic_lemma(bool derived) {
-    if (basic_sign_lemma(derived))
-        return true;
-    if (derived)
-        return false;
-    init_rm_to_refine();
-    const auto& rm_ref = m_rm_table.to_refine();
-    TRACE("nla_solver", tout << "rm_ref = "; print_vector(rm_ref, tout););
-    unsigned start = random() % rm_ref.size();
-    unsigned i = start;
-    do {
-        const rooted_mon& r = m_rm_table.rms()[rm_ref[i]];
-        SASSERT (!check_monomial(m_monomials[r.orig_index()]));
-        basic_lemma_for_mon(r, derived);
-        if (++i == rm_ref.size()) {
-            i = 0;
-        }
-    } while(i != start && !done());
-        
-    return false;
-}
-
-void core::map_monomial_vars_to_monomial_indices(unsigned i) {
-    const monomial& m = m_monomials[i];
-    for (lpvar j : m.vars()) {
-        auto it = m_monomials_containing_var.find(j);
-        if (it == m_monomials_containing_var.end()) {
-            unsigned_vector ms;
-            ms.push_back(i);
-            m_monomials_containing_var[j] = ms;
-        }
-        else {
-            it->second.push_back(i);
-        }
-    }
-}
-
-void core::map_vars_to_monomials() {
-    for (unsigned i = 0; i < m_monomials.size(); i++) {
-        const monomial& m = m_monomials[i];
-        lpvar v = m.var();
-        SASSERT(m_var_to_its_monomial.find(v) == m_var_to_its_monomial.end());
-        m_var_to_its_monomial[v] = i;
-        map_monomial_vars_to_monomial_indices(i);
-    }
-}
 
 // we look for octagon constraints here, with a left part  +-x +- y 
 void core::collect_equivs() {
@@ -1494,38 +1380,6 @@ void core::init_vars_equivalence() {
         
     SASSERT((settings().random_next() % 100) || tables_are_ok());
 }
-
-bool core:: vars_table_is_ok() const {
-    for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) {
-        auto it = m_var_to_its_monomial.find(j);
-        if (it != m_var_to_its_monomial.end()
-            && m_monomials[it->second].var() != j) {
-            TRACE("nla_solver", tout << "j = ";
-                  print_var(j, tout););
-            return false;
-        }
-    }
-    for (unsigned i = 0; i < m_monomials.size(); i++){
-        const monomial& m = m_monomials[i];
-        lpvar j = m.var();
-        if (m_var_to_its_monomial.find(j) == m_var_to_its_monomial.end()){
-            return false;
-        }
-    }
-    return true;
-}
-
-bool core:: rm_table_is_ok() const {
-    for (const auto & rm : m_rm_table.rms()) {
-        for (lpvar j : rm.vars()) {
-            if (!m_evars.is_root(j)){
-                TRACE("nla_solver", print_var(j, tout););
-                return false;
-            }
-        }
-    }
-    return true;
-}
     
 bool core:: tables_are_ok() const {
     return vars_table_is_ok() && rm_table_is_ok();
@@ -1543,26 +1397,14 @@ bool core:: vars_are_roots(const T& v) const {
 }
 
 
-void core::register_monomial_in_tables(unsigned i_mon) {
-    const monomial& m = m_monomials[i_mon];
-    monomial_coeff mc = canonize_monomial(m);
-    TRACE("nla_solver_rm", tout << "i_mon = " << i_mon << ", mon = ";
-          print_monomial(m_monomials[i_mon], tout);
-          tout << "\nmc = ";
-          print_product(mc.vars(), tout);
-          );
-    m_rm_table.register_key_mono_in_rooted_monomials(mc, i_mon);        
-}
 
 template <typename T>
 void core::trace_print_rms(const T& p, std::ostream& out) {
-    out << "p = {";
+    out << "p = {\n";
     for (auto j : p) {
-        out << "\nj = " << j <<
-            ", rm = ";
-        print_rooted_monomial(m_rm_table.rms()[j], out);
+        out << "j = " << j << ", rm = " << m_emons.canonical[j] << "\n";
     }
-    out << "\n}";
+    out << "}";
 }
 
 void core::print_monomial_stats(const monomial& m, std::ostream& out) {
@@ -1572,8 +1414,8 @@ void core::print_monomial_stats(const monomial& m, std::ostream& out) {
         if (abs(vvr(mc.vars()[i])) == rational(1)) {
             auto vv = mc.vars();
             vv.erase(vv.begin()+i);
-            auto it = m_rm_table.vars_key_to_rm_index().find(vv);
-            if (it == m_rm_table.vars_key_to_rm_index().end()) {
+            signed_vars const* sv = m_emons.find_canonical(vv);
+            if (!sv) {
                 out << "nf length" << vv.size() << "\n"; ;
             }
         }
@@ -1581,32 +1423,16 @@ void core::print_monomial_stats(const monomial& m, std::ostream& out) {
 }
     
 void core::print_stats(std::ostream& out) {
-    // for (const auto& m : m_monomials) 
-    //     print_monomial_stats(m, out);
-    m_rm_table.print_stats(out);
 }
         
-void core::register_monomials_in_tables() {
-    for (unsigned i = 0; i < m_monomials.size(); i++) 
-        register_monomial_in_tables(i);
-
-    m_rm_table.fill_rooted_monomials_containing_var();
-    m_rm_table.fill_proper_multiples();
-    TRACE("nla_solver_rm", print_stats(tout););
-}
 
 void core::clear() {
-    m_var_to_its_monomial.clear();
-    m_rm_table.clear();
-    m_monomials_containing_var.clear();
     m_lemma_vec->clear();
 }
     
 void core::init_search() {
     clear();
-    map_vars_to_monomials();
     init_vars_equivalence();
-    register_monomials_in_tables();
 }
 
 void core::init_to_refine() {
@@ -1617,15 +1443,16 @@ void core::init_to_refine() {
     
     TRACE("nla_solver", 
           tout << m_to_refine.size() << " mons to refine:\n";
-          for (unsigned v : m_to_refine) tout << m_emons.var2monomial(v) << "\n";);
+          for (lpvar v : m_to_refine) tout << m_emons[v] << "\n";);
 }
         
 std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
     std::unordered_set<lpvar> vars;
     auto insert_j = [&](lpvar j) { 
         vars.insert(j);
-        auto const* m = m_emons.var2monomial(j);
-        if (m) for (lpvar k : *m) vars.insert(k);
+        if (m_emons.is_monomial_var(j)) {
+            for (lpvar k : m_emons[j]) vars.insert(k);
+        }
     };
     
     for (const auto& i : current_lemma().ineqs()) {
@@ -1642,7 +1469,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
     return vars;
 }
 
-bool core:: divide(const rooted_mon& bc, const factor& c, factor & b) const {
+bool core::divide(const signed_vars& bc, const factor& c, factor & b) const {
     svector<lpvar> c_vars = sorted_vars(c);
     TRACE("nla_solver_div",
           tout << "c_vars = ";
@@ -1659,12 +1486,12 @@ bool core:: divide(const rooted_mon& bc, const factor& c, factor & b) const {
         b = factor(b_vars[0]);
         return true;
     }
-    auto it = m_rm_table.vars_key_to_rm_index().find(b_vars);
-    if (it == m_rm_table.vars_key_to_rm_index().end()) {
+    signed_vars const* sv = m_emons.find_canonical(b_vars);
+    if (!sv) {
         TRACE("nla_solver_div", tout << "not in rooted";);
         return false;
     }
-    b = factor(it->second, factor_type::RM);
+    b = factor(sv->var(), factor_type::RM);
     TRACE("nla_solver_div", tout << "success div:"; print_factor(b, tout););
     return true;
 }
@@ -1709,17 +1536,15 @@ void core::print_specific_lemma(const lemma& l, std::ostream& out) const {
 }
     
 
-void core::trace_print_ol(const rooted_mon& ac,
+void core::trace_print_ol(const signed_vars& ac,
                           const factor& a,
                           const factor& c,
-                          const rooted_mon& bc,
+                          const signed_vars& bc,
                           const factor& b,
                           std::ostream& out) {
-    out << "ac = ";
-    print_rooted_monomial_with_vars(ac, out);
-    out << "\nbc = ";
-    print_rooted_monomial_with_vars(bc, out);
-    out << "\na = ";
+    out << "ac = " << ac << "\n";
+    out << "bc = " << bc << "\n";
+    out << "a = ";
     print_factor_with_vars(a, out);
     out << ", \nb = ";
     print_factor_with_vars(b, out);
@@ -1733,20 +1558,15 @@ void core::maybe_add_a_factor(lpvar i,
                               std::unordered_set<unsigned>& found_rm,
                               vector<factor> & r) const {
     SASSERT(abs(vvr(i)) == abs(vvr(c)));
-    auto it = m_var_to_its_monomial.find(i);
-    if (it == m_var_to_its_monomial.end()) {
+    if (!m_emons.is_monomial_var(i)) {
         i = m_evars.find(i).var();
         if (try_insert(i, found_vars)) {
             r.push_back(factor(i, factor_type::VAR));
         }
     } else {
-        SASSERT(m_monomials[it->second].var() == i && abs(vvr(m_monomials[it->second])) == abs(vvr(c)));
-        const index_with_sign & i_s = m_rm_table.get_rooted_mon(it->second);
-        unsigned rm_i = i_s.index();
-        //                SASSERT(abs(vvr(m_rm_table.rms()[i])) == abs(vvr(c)));
-        if (try_insert(rm_i, found_rm)) {
-            r.push_back(factor(rm_i, factor_type::RM));
-            TRACE("nla_solver", tout << "inserting factor = "; print_factor_with_vars(factor(rm_i, factor_type::RM), tout); );
+        if (try_insert(i, found_rm)) {
+            r.push_back(factor(i, factor_type::RM));
+            TRACE("nla_solver", tout << "inserting factor = "; print_factor_with_vars(factor(i, factor_type::RM), tout); );
         }
     }
 }
@@ -1755,21 +1575,21 @@ void core::maybe_add_a_factor(lpvar i,
 // Returns rooted monomials by arity
 std::unordered_map<unsigned, unsigned_vector> core::get_rm_by_arity() {
     std::unordered_map<unsigned, unsigned_vector> m;
-    for (unsigned i = 0; i < m_rm_table.rms().size(); i++ ) {
-        unsigned arity = m_rm_table.rms()[i].vars().size();
+    for (auto const& mon : m_emons) {
+        unsigned arity = mon.vars().size();
         auto it = m.find(arity);
         if (it == m.end()) {
             it = m.insert(it, std::make_pair(arity, unsigned_vector()));
         }
-        it->second.push_back(i);
+        it->second.push_back(mon.var());
     }
     return m;
 }
 
     
 
-bool core:: rm_check(const rooted_mon& rm) const {
-    return check_monomial(m_monomials[rm.orig_index()]);
+bool core::rm_check(const signed_vars& rm) const {
+    return check_monomial(m_emons[rm.var()]);
 }
     
 
@@ -1817,6 +1637,7 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
     mk_ineq(t, cmp, abs(bound));
 }
 
+// NB - move this comment to monotonicity or appropriate.
 /** \brief enforce the inequality |m| <= product |m[i]| .
     by enforcing lemma:
     /\_i |m[i]| <= |vvr(m[i])| => |m| <= |product_i vvr(m[i])|
@@ -1825,7 +1646,7 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
 */
 
     
-bool core:: find_bfc_to_refine_on_rmonomial(const rooted_mon& rm, bfc & bf) {
+bool core::find_bfc_to_refine_on_rmonomial(const signed_vars& rm, bfc & bf) {
     for (auto factorization : factorization_factory_imp(rm, *this)) {
         if (factorization.size() == 2) {
             auto a = factorization[0];
@@ -1839,13 +1660,14 @@ bool core:: find_bfc_to_refine_on_rmonomial(const rooted_mon& rm, bfc & bf) {
     return false;
 }
     
-bool core:: find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const rooted_mon*& rm_found){
-    for (unsigned i: m_rm_table.to_refine()) {
-        const auto& rm = m_rm_table.rms()[i]; 
-        SASSERT (!check_monomial(m_monomials[rm.orig_index()]));
+bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const signed_vars*& rm_found){
+    rm_found = nullptr;
+    for (unsigned i: m_to_refine) {
+        const auto& rm = m_emons.canonical[i];
+        SASSERT (!check_monomial(m_emons[rm.var()]));
         if (rm.size() == 2) {
             sign = rational(1);
-            const monomial & m = m_monomials[rm.orig_index()];
+            const monomial & m = m_emons[rm.var()];
             j = m.var();
             rm_found = nullptr;
             bf.m_x = factor(m[0]);
@@ -1855,10 +1677,10 @@ bool core:: find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const rooted_m
                 
         rm_found = &rm;
         if (find_bfc_to_refine_on_rmonomial(rm, bf)) {
-            j = m_monomials[rm.orig_index()].var();
-            sign = rm.orig_sign();
+            j = rm.var();
+            sign = rm.rsign();
             TRACE("nla_solver", tout << "found bf";
-                  tout << ":rm:"; print_rooted_monomial(rm, tout) << "\n";
+                  tout << ":rm:" << rm << "\n";
                   tout << "bf:"; print_bfc(bf, tout);
                   tout << ", product = " << vvr(rm) << ", but should be =" << vvr(bf.m_x)*vvr(bf.m_y);
                   tout << ", j == "; print_var(j, tout) << "\n";);
@@ -2159,3 +1981,10 @@ lbool core::test_check(
 template rational core::product_value<monomial>(const monomial & m) const;
 
 } // end of nla
+
+
+#if 0
+rational core::mon_value_by_vars(unsigned i) const {
+    return product_value(m_monomials[i]);
+}
+#endif
diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h
index 2272716a6..d5f288f74 100644
--- a/src/util/lp/nla_core.h
+++ b/src/util/lp/nla_core.h
@@ -21,7 +21,6 @@
 #include "util/lp/factorization.h"
 #include "util/lp/lp_types.h"
 #include "util/lp/var_eqs.h"
-#include "util/lp/rooted_mons.h"
 #include "util/lp/nla_tangent_lemmas.h"
 #include "util/lp/nla_basics_lemmas.h"
 #include "util/lp/nla_order_lemmas.h"
@@ -38,8 +37,8 @@ bool try_insert(const A& elem, B& collection) {
     return true;
 }
 
-typedef lp::constraint_index lpci;
-typedef lp::lconstraint_kind llc;
+typedef lp::constraint_index     lpci;
+typedef lp::lconstraint_kind     llc;
 typedef lp::constraint_index     lpci;
 typedef lp::explanation          expl_set;
 typedef lp::var_index            lpvar;
@@ -75,29 +74,20 @@ public:
 };
 
 
-struct core {
-    //fields    
-    var_eqs                                                          m_evars;
-    vector<monomial>                                                 m_monomials;
+class core {
+public:
+    var_eqs                  m_evars;
+    emonomials               m_emons;
+    lp::lar_solver           m_lar_solver;
+    vector<lemma> *          m_lemma_vec;
+    svector<lpvar>           m_to_refine;
+    tangents                 m_tangents;
+    basics                   m_basics;
+    order                    m_order;
+    monotone                 m_monotone;
 
-    // this field is used for the push/pop operations
-    unsigned_vector                                                  m_monomials_counts;
-    lp::lar_solver&                                                  m_lar_solver;
-    std::unordered_map<lpvar, svector<lpvar>>                        m_monomials_containing_var;
-    
-    // m_var_to_its_monomial[m_monomials[i].var()] = i
-    std::unordered_map<lpvar, unsigned>                              m_var_to_its_monomial;
-    vector<lemma> *                                                  m_lemma_vec;
-    unsigned_vector                                                  m_to_refine;
-    std::unordered_map<unsigned_vector, unsigned, hash_svector>      m_mkeys; // the key is the sorted vars of a monomial 
-    tangents                                                         m_tangents;
-    basics                                                           m_basics;
-    order                                                           m_order;
-    monotone                                                        m_monotone;
-    emonomials                                                       m_emons;
-    // methods
     core(lp::lar_solver& s);
-    
+
     bool compare_holds(const rational& ls, llc cmp, const rational& rs) const;
     
     rational value(const lp::lar_term& r) const;
@@ -112,13 +102,13 @@ struct core {
 
     lp::impq vv(lpvar j) const { return m_lar_solver.get_column_value(j); }
     
-    lpvar var(const rooted_mon& rm) const {return m_monomials[rm.orig_index()].var(); }
+    lpvar var(signed_vars const& sv) const { return sv.var(); }
 
-    rational vvr(const rooted_mon& rm) const { return vvr(m_monomials[rm.orig_index()].var()) * rm.orig_sign(); }
+    rational vvr(const signed_vars& rm) const { return vvr(m_emons[rm.var()]); } // NB: removed multiplication with sign.
 
-   rational vvr(const factor& f) const {  return f.is_var()? vvr(f.index()) : vvr(m_rm_table.rms()[f.index()]); }
+    rational vvr(const factor& f) const {  return f.is_var()? vvr(f.var()) : vvr(m_emons[f.var()]); }
 
-    lpvar var(const factor& f) const { return f.is_var()? f.index() : var(m_rm_table.rms()[f.index()]); }
+    lpvar var(const factor& f) const { return f.var(); }
 
     svector<lpvar> sorted_vars(const factor& f) const;
     bool done() const;
@@ -132,17 +122,16 @@ struct core {
     
     // the value of the rooted monomias is equal to the value of the variable multiplied
     // by the canonize_sign
-    rational canonize_sign(const rooted_mon& m) const;
+    rational canonize_sign(const signed_vars& m) const;
     
-    // returns the monomial index
-    unsigned add(lpvar v, unsigned sz, lpvar const* vs);
-    
-    void push();
 
-    void deregister_monomial_from_rooted_monomials (const monomial & m, unsigned i);
+    void deregister_monomial_from_signed_varsomials (const monomial & m, unsigned i);
 
     void deregister_monomial_from_tables(const monomial & m, unsigned i);
-     
+
+    // returns the monomial index
+    void add(lpvar v, unsigned sz, lpvar const* vs);   
+    void push();     
     void pop(unsigned n);
 
     rational mon_value_by_vars(unsigned i) const;
@@ -153,7 +142,7 @@ struct core {
     bool check_monomial(const monomial& m) const;
     
     void explain(const monomial& m, lp::explanation& exp) const;
-    void explain(const rooted_mon& rm, lp::explanation& exp) const;
+    void explain(const signed_vars& rm, lp::explanation& exp) const;
     void explain(const factor& f, lp::explanation& exp) const;
     void explain(lpvar j, lp::explanation& exp) const;
     void explain_existing_lower_bound(lpvar j);
@@ -179,12 +168,10 @@ struct core {
     template <typename T>
     std::ostream& print_product_with_vars(const T& m, std::ostream& out) const;
     std::ostream& print_monomial_with_vars(const monomial& m, std::ostream& out) const;
-    std::ostream& print_rooted_monomial(const rooted_mon& rm, std::ostream& out) const;
-    std::ostream& print_rooted_monomial_with_vars(const rooted_mon& rm, std::ostream& out) const;
     std::ostream& print_explanation(const lp::explanation& exp, std::ostream& out) const;
     template <typename T>
     void trace_print_rms(const T& p, std::ostream& out);
-    void trace_print_monomial_and_factorization(const rooted_mon& rm, const factorization& f, std::ostream& out) const;
+    void trace_print_monomial_and_factorization(const signed_vars& rm, const factorization& f, std::ostream& out) const;
     void print_monomial_stats(const monomial& m, std::ostream& out);    
     void print_stats(std::ostream& out);
     std::ostream& print_lemma(std::ostream& out) const;
@@ -192,10 +179,10 @@ struct core {
     void print_specific_lemma(const lemma& l, std::ostream& out) const;
     
 
-    void trace_print_ol(const rooted_mon& ac,
+    void trace_print_ol(const signed_vars& ac,
                         const factor& a,
                         const factor& c,
-                        const rooted_mon& bc,
+                        const signed_vars& bc,
                         const factor& b,
                         std::ostream& out);
 
@@ -258,7 +245,7 @@ struct core {
     const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
 
 
-    int get_derived_sign(const rooted_mon& rm, const factorization& f) const;
+    int get_derived_sign(const signed_vars& rm, const factorization& f) const;
 
 
     bool var_has_positive_lower_bound(lpvar j) const;
@@ -289,7 +276,7 @@ struct core {
 
     template <typename T>
     bool mon_has_zero(const T& product) const;
-    void init_rm_to_refine();
+    void init_rm_to_refine() { NOT_IMPLEMENTED_YET(); }
     lp::lp_settings& settings();
     unsigned random();
     void map_monomial_vars_to_monomial_indices(unsigned i);
@@ -328,7 +315,7 @@ struct core {
 
     void init_to_refine();
 
-    bool divide(const rooted_mon& bc, const factor& c, factor & b) const;
+    bool divide(const signed_vars& bc, const factor& c, factor & b) const;
 
     void negate_factor_equality(const factor& c, const factor& d);
     
@@ -336,15 +323,15 @@ struct core {
 
     std::unordered_set<lpvar> collect_vars(const lemma& l) const;
 
-    bool rm_check(const rooted_mon&) const;
+    bool rm_check(const signed_vars&) const;
     std::unordered_map<unsigned, unsigned_vector> get_rm_by_arity();
 
     void add_abs_bound(lpvar v, llc cmp);
     void add_abs_bound(lpvar v, llc cmp, rational const& bound);
 
-    bool  find_bfc_to_refine_on_rmonomial(const rooted_mon& rm, bfc & bf);
+    bool  find_bfc_to_refine_on_rmonomial(const signed_vars& rm, bfc & bf);
     
-    bool  find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const rooted_mon*& rm_found);
+    bool  find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const signed_vars*& rm_found);
     void generate_simple_sign_lemma(const rational& sign, const monomial& m);
 
     void negate_relation(unsigned j, const rational& a);
diff --git a/src/util/lp/nla_monotone_lemmas.cpp b/src/util/lp/nla_monotone_lemmas.cpp
index 0766be4d0..c531e88b0 100644
--- a/src/util/lp/nla_monotone_lemmas.cpp
+++ b/src/util/lp/nla_monotone_lemmas.cpp
@@ -19,7 +19,7 @@
   --*/
 #include "util/lp/nla_basics_lemmas.h"
 #include "util/lp/nla_core.h"
-#include "util/lp/factorization_factory_imp.h"
+// #include "util/lp/factorization_factory_imp.h"
 namespace nla {
 
 monotone::monotone(core * c) : common(c) {}
@@ -33,18 +33,15 @@ void monotone::print_monotone_array(const vector<std::pair<std::vector<rational>
     }
     out <<  "}";
 }
-bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const rooted_mon& rm) {
+bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm) {
     const rational v = abs(vvr(rm));
     const auto& key = lex_sorted[i].first;
-    TRACE("nla_solver", tout << "rm = ";
-          print_rooted_monomial_with_vars(rm, tout); tout << "i = " << i << std::endl;);
+    TRACE("nla_solver", tout << "rm = " << rm << "i = " << i << std::endl;);
     for (unsigned k = i + 1; k < lex_sorted.size(); k++) {
         const auto& p = lex_sorted[k];
-        const rooted_mon& rmk = c().m_rm_table.rms()[p.second];
+        const signed_vars& rmk = c().m_emons.canonical[p.second];
         const rational vk = abs(vvr(rmk));
-        TRACE("nla_solver", tout << "rmk = ";
-              print_rooted_monomial_with_vars(rmk, tout);
-              tout << "\n";
+        TRACE("nla_solver", tout << "rmk = " << rmk << "\n";
               tout << "vk = " << vk << std::endl;);
         if (vk > v) continue;
         unsigned strict;
@@ -64,19 +61,16 @@ bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<
     return false;
 }
 
-bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const rooted_mon& rm) {
+bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm) {
     const rational v = abs(vvr(rm));
     const auto& key = lex_sorted[i].first;
-    TRACE("nla_solver", tout << "rm = ";
-          print_rooted_monomial_with_vars(rm, tout); tout << "i = " << i << std::endl;);
+    TRACE("nla_solver", tout << "rm = " << rm << "i = " << i << std::endl;);
         
     for (unsigned k = i; k-- > 0;) {
         const auto& p = lex_sorted[k];
-        const rooted_mon& rmk = c().m_rm_table.rms()[p.second];
+        const signed_vars& rmk = c().m_emons.canonical[p.second];
         const rational vk = abs(vvr(rmk));
-        TRACE("nla_solver", tout << "rmk = ";
-              print_rooted_monomial_with_vars(rmk, tout);
-              tout << "\n";
+        TRACE("nla_solver", tout << "rmk = " << rmk << "\n";
               tout << "vk = " << vk << std::endl;);
         if (vk < v) continue;
         unsigned strict;
@@ -98,22 +92,22 @@ bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<
     return false;
 }
 
-bool monotone::monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const rooted_mon& rm) {
+bool monotone::monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm) {
     return monotonicity_lemma_on_lex_sorted_rm_upper(lex_sorted, i, rm)
         || monotonicity_lemma_on_lex_sorted_rm_lower(lex_sorted, i, rm);
 }
 bool monotone::monotonicity_lemma_on_lex_sorted(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted) {
     for (unsigned i = 0; i < lex_sorted.size(); i++) {
         unsigned rmi = lex_sorted[i].second;
-        const rooted_mon& rm = c().m_rm_table.rms()[rmi];
-        TRACE("nla_solver", print_rooted_monomial(rm, tout); tout << "\n, rm_check = " << c().rm_check(rm); tout << std::endl;); 
+        const signed_vars& rm = c().m_emons.canonical[rmi];
+        TRACE("nla_solver", tout << rm << "\n, rm_check = " << c().rm_check(rm); tout << std::endl;); 
         if ((!c().rm_check(rm)) && monotonicity_lemma_on_lex_sorted_rm(lex_sorted, i, rm))
             return true;
     }
     return false;
 }
 
-vector<std::pair<rational, lpvar>> monotone::get_sorted_key_with_vars(const rooted_mon& a) const {
+vector<std::pair<rational, lpvar>> monotone::get_sorted_key_with_vars(const signed_vars& a) const {
     vector<std::pair<rational, lpvar>> r;
     for (lpvar j : a.vars()) {
         r.push_back(std::make_pair(abs(vvr(j)), j));
@@ -143,8 +137,8 @@ void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
 }
 
 // strict version
-void monotone::generate_monl_strict(const rooted_mon& a,
-                                const rooted_mon& b,
+void monotone::generate_monl_strict(const signed_vars& a,
+                                const signed_vars& b,
                                 unsigned strict) {
     add_empty_lemma();
     auto akey = get_sorted_key_with_vars(a);
@@ -165,8 +159,8 @@ void monotone::generate_monl_strict(const rooted_mon& a,
 }
 
 void monotone::assert_abs_val_a_le_abs_var_b(
-    const rooted_mon& a,
-    const rooted_mon& b,
+    const signed_vars& a,
+    const signed_vars& b,
     bool strict) {
     lpvar aj = var(a);
     lpvar bj = var(b);
@@ -194,11 +188,11 @@ void monotone::negate_abs_a_lt_abs_b(lpvar a, lpvar b) {
 
 
 // not a strict version
-void monotone::generate_monl(const rooted_mon& a,
-                         const rooted_mon& b) {
-    TRACE("nla_solver", tout <<
-          "a = "; print_rooted_monomial_with_vars(a, tout) << "\n:";
-          tout << "b = "; print_rooted_monomial_with_vars(a, tout) << "\n:";);
+void monotone::generate_monl(const signed_vars& a,
+                         const signed_vars& b) {
+    TRACE("nla_solver", 
+          tout << "a = " << a << "\n:";
+          tout << "b = " << b << "\n:";);
     add_empty_lemma();
     auto akey = get_sorted_key_with_vars(a);
     auto bkey = get_sorted_key_with_vars(b);
@@ -212,7 +206,7 @@ void monotone::generate_monl(const rooted_mon& a,
     TRACE("nla_solver", print_lemma(tout););
 }
 
-std::vector<rational> monotone::get_sorted_key(const rooted_mon& rm) const {
+std::vector<rational> monotone::get_sorted_key(const signed_vars& rm) const {
     std::vector<rational> r;
     for (unsigned j : rm.vars()) {
         r.push_back(abs(vvr(j)));
@@ -224,7 +218,7 @@ std::vector<rational> monotone::get_sorted_key(const rooted_mon& rm) const {
 bool monotone::monotonicity_lemma_on_rms_of_same_arity(const unsigned_vector& rms) { 
     vector<std::pair<std::vector<rational>, unsigned>> lex_sorted;
     for (unsigned i : rms) {
-        lex_sorted.push_back(std::make_pair(get_sorted_key(c().m_rm_table.rms()[i]), i));
+        lex_sorted.push_back(std::make_pair(get_sorted_key(c().m_emons.canonical[i]), i));
     }
     std::sort(lex_sorted.begin(), lex_sorted.end(),
               [](const std::pair<std::vector<rational>, unsigned> &a,
@@ -237,10 +231,10 @@ bool monotone::monotonicity_lemma_on_rms_of_same_arity(const unsigned_vector& rm
     
 void monotone::monotonicity_lemma() {
     unsigned shift = random();
-    unsigned size = c().m_rm_table.m_to_refine.size();
+    unsigned size = c().m_to_refine.size();
     for(unsigned i = 0; i < size && !done(); i++) { 
-        unsigned rm_i = c().m_rm_table.m_to_refine[(i + shift)% size];
-        monotonicity_lemma(c().m_rm_table.rms()[rm_i].orig_index());
+        lpvar v = c().m_to_refine[(i + shift) % size];
+        monotonicity_lemma(c().m_emons[v]);
     }
 }
 
@@ -257,8 +251,7 @@ void monotone::monotonicity_lemma() {
 
 #endif
 
-void monotone::monotonicity_lemma(unsigned i_mon) {
-    const monomial & m = c().m_monomials[i_mon];
+void monotone::monotonicity_lemma(monomial const& m) {
     SASSERT(!check_monomial(m));
     if (c().mon_has_zero(m))
         return;
diff --git a/src/util/lp/nla_monotone_lemmas.h b/src/util/lp/nla_monotone_lemmas.h
index 61e2e2339..a36144e2d 100644
--- a/src/util/lp/nla_monotone_lemmas.h
+++ b/src/util/lp/nla_monotone_lemmas.h
@@ -19,26 +19,26 @@
   --*/
 #pragma once
 namespace nla {
-struct core;
+class core;
 struct monotone: common {    
     monotone(core *core);
     void print_monotone_array(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted,
                                   std::ostream& out) const;
-    bool monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const rooted_mon& rm);
-    bool monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const rooted_mon& rm);
-    bool monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const rooted_mon& rm);
+    bool monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm);
+    bool monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm);
+    bool monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm);
     bool monotonicity_lemma_on_lex_sorted(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted);
     bool  monotonicity_lemma_on_rms_of_same_arity(const unsigned_vector& rms);
     void monotonicity_lemma();
-    void monotonicity_lemma(unsigned i_mon);
+    void monotonicity_lemma(monomial const& m);
     void monotonicity_lemma_gt(const monomial& m, const rational& prod_val);    
     void monotonicity_lemma_lt(const monomial& m, const rational& prod_val);    
-    void generate_monl_strict(const rooted_mon& a, const rooted_mon& b,  unsigned strict);
-    void generate_monl(const rooted_mon& a, const rooted_mon& b);
-    std::vector<rational> get_sorted_key(const rooted_mon& rm) const;
-    vector<std::pair<rational, lpvar>> get_sorted_key_with_vars(const rooted_mon& a) const;
+    void generate_monl_strict(const signed_vars& a, const signed_vars& b,  unsigned strict);
+    void generate_monl(const signed_vars& a, const signed_vars& b);
+    std::vector<rational> get_sorted_key(const signed_vars& rm) const;
+    vector<std::pair<rational, lpvar>> get_sorted_key_with_vars(const signed_vars& a) const;
     void negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict);
     void negate_abs_a_lt_abs_b(lpvar a, lpvar b);
-    void assert_abs_val_a_le_abs_var_b(const rooted_mon& a, const rooted_mon& b, bool strict);
+    void assert_abs_val_a_le_abs_var_b(const signed_vars& a, const signed_vars& b, bool strict);
 };
 }
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index 6a30ce5b1..2f6739681 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -29,38 +29,35 @@ namespace nla {
 // a >< b && c < 0  => ac <> bc
 // ac[k] plays the role of c   
 
-bool order::order_lemma_on_ac_and_bc(const rooted_mon& rm_ac,
+bool order::order_lemma_on_ac_and_bc(const signed_vars& rm_ac,
                                      const factorization& ac_f,
                                      unsigned k,
-                                     const rooted_mon& rm_bd) {
-    TRACE("nla_solver",   tout << "rm_ac = ";
-          c().print_rooted_monomial(rm_ac, tout);
-          tout << "\nrm_bd = ";
-          c().print_rooted_monomial(rm_bd, tout);
-          tout << "\nac_f[k] = ";
+                                     const signed_vars& rm_bd) {
+    TRACE("nla_solver", 
+          tout << "rm_ac = " << rm_ac << "\n";
+          tout << "rm_bd = " << rm_bd << "\n";
+          tout << "ac_f[k] = ";
           c().print_factor_with_vars(ac_f[k], tout););
     factor b;
-    if (!c().divide(rm_bd, ac_f[k], b)){
-        return false;
-    }
-
-    return order_lemma_on_ac_and_bc_and_factors(rm_ac, ac_f[(k + 1) % 2], ac_f[k], rm_bd, b);
+    return 
+        c().divide(rm_bd, ac_f[k], b) && 
+        order_lemma_on_ac_and_bc_and_factors(rm_ac, ac_f[(k + 1) % 2], ac_f[k], rm_bd, b);
 }
 
-bool order::order_lemma_on_ac_explore(const rooted_mon& rm, const factorization& ac, unsigned k) {
+bool order::order_lemma_on_ac_explore(const signed_vars& rm, const factorization& ac, unsigned k) {
     const factor c = ac[k];
     TRACE("nla_solver", tout << "c = "; _().print_factor_with_vars(c, tout); );
     if (c.is_var()) {
         TRACE("nla_solver", tout << "var(c) = " << var(c););
-        for (unsigned rm_bc : _().m_rm_table.var_map()[c.index()]) {
-            TRACE("nla_solver", );
-            if (order_lemma_on_ac_and_bc(rm ,ac, k, _().m_rm_table.rms()[rm_bc])) {
+        for (monomial const& bc : _().m_emons.get_use_list(c.var())) {
+            if (order_lemma_on_ac_and_bc(rm ,ac, k, _().m_emons.canonical[bc])) {
                 return true;
             }
         }
-    } else {
-        for (unsigned rm_bc : _().m_rm_table.proper_multiples()[c.index()]) {
-            if (order_lemma_on_ac_and_bc(rm , ac, k, _().m_rm_table.rms()[rm_bc])) {
+    } 
+    else {
+        for (monomial const& bc : _().m_emons.get_factors_of(c.var())) {
+            if (order_lemma_on_ac_and_bc(rm , ac, k, _().m_emons.canonical[bc])) {
                 return true;
             }
         }
@@ -68,11 +65,11 @@ bool order::order_lemma_on_ac_explore(const rooted_mon& rm, const factorization&
     return false;
 }
 
-void order::order_lemma_on_factorization(const rooted_mon& rm, const factorization& ab) {
-    const monomial& m = _().m_monomials[rm.orig_index()];
-    TRACE("nla_solver", tout << "orig_sign = " << rm.orig_sign() << "\n";);
-    rational sign = rm.orig_sign();
-    for(factor f: ab)
+void order::order_lemma_on_factorization(const signed_vars& rm, const factorization& ab) {
+    const monomial& m = _().m_emons[rm.var()];
+    TRACE("nla_solver", tout << "orig_sign = " << _().m_emons.orig_sign(rm) << "\n";);
+    rational sign = _().m_emons.orig_sign(rm);
+    for (factor f: ab)
         sign *= _().canonize_sign(f);
     const rational & fv = vvr(ab[0]) * vvr(ab[1]);
     const rational mv = sign * vvr(m);
@@ -93,11 +90,11 @@ void order::order_lemma_on_factorization(const rooted_mon& rm, const factorizati
 }
 // |c_sign| = 1, and c*c_sign > 0
 // ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
-void order::generate_ol(const rooted_mon& ac,                     
+void order::generate_ol(const signed_vars& ac,                     
                        const factor& a,
                        int c_sign,
                        const factor& c,
-                       const rooted_mon& bc,
+                       const signed_vars& bc,
                        const factor& b,
                        llc ab_cmp) {
     add_empty_lemma();
@@ -117,7 +114,7 @@ void order::generate_mon_ol(const monomial& ac,
                            lpvar a,
                            const rational& c_sign,
                            lpvar c,
-                           const rooted_mon& bd,
+                           const signed_vars& bd,
                            const factor& b,
                            const rational& d_sign,
                            lpvar d,
@@ -142,22 +139,19 @@ void order::negate_var_factor_relation(const rational& a_sign, lpvar a, const ra
 void order::order_lemma() {
     TRACE("nla_solver", );
     c().init_rm_to_refine();
-    const auto& rm_ref = c().m_rm_table.to_refine();
-    unsigned start = random() % rm_ref.size();
-    unsigned i = start;
-    do {
-        const rooted_mon& rm = c().m_rm_table.rms()[rm_ref[i]];
+    const auto& rm_ref = c().m_to_refine;
+    unsigned start = random();
+    unsigned sz = rm_ref.size();
+    for (unsigned i = sz; i-- > 0 && !done(); ) {        
+        const signed_vars& rm = c().m_emons.canonical[rm_ref[(i + start) % sz]];
         order_lemma_on_rmonomial(rm);
-        if (++i == rm_ref.size()) {
-            i = 0;
-        }
-    } while(i != start && !done());
+    }
 }
 
-bool order::order_lemma_on_ac_and_bc_and_factors(const rooted_mon& ac,
+bool order::order_lemma_on_ac_and_bc_and_factors(const signed_vars& ac,
                                                  const factor& a,
                                                  const factor& c,
-                                                 const rooted_mon& bc,
+                                                 const signed_vars& bc,
                                                  const factor& b) {
     auto cv = vvr(c); 
     int c_sign = nla::rat_sign(cv);
@@ -239,10 +233,10 @@ void order::order_lemma_on_ab(const monomial& m, const rational& sign, lpvar a,
         order_lemma_on_ab_lt(m, sign, a, b);
 }
 // a > b && c > 0 => ac > bc
-void order::order_lemma_on_rmonomial(const rooted_mon& rm) {
+void order::order_lemma_on_rmonomial(const signed_vars& rm) {
     TRACE("nla_solver_details",
           tout << "rm = "; print_product(rm, tout);
-          tout << ", orig = "; print_monomial(c().m_monomials[rm.orig_index()], tout);
+          tout << ", orig = " << c().m_emons[rm.var()] << "\n";
           );
     for (auto ac : factorization_factory_imp(rm, c())) {
         if (ac.size() != 2)
@@ -273,17 +267,18 @@ void order::order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, i
     mk_ineq(ac.var(), - vvr(x), y, sign == 1?llc::LE:llc::GE);
     TRACE("nla_solver", print_lemma(tout););
 }
-void order::order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const rooted_mon& rm_bd) {
+void order::order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const monomial& bd) {
+    signed_vars const& rm_bd = _().m_emons.canonical[bd];
     factor d(_().m_evars.find(ac[k]).var(), factor_type::VAR);
     factor b;
-    if (!_().divide(rm_bd, d, b))
-        return;
-    order_lemma_on_binomial_ac_bd(ac, k, rm_bd, b, d.index());
+    if (_().divide(rm_bd, d, b)) {
+        order_lemma_on_binomial_ac_bd(ac, k, rm_bd, b, d.var());
+    }
 }
 
-void order::order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const rooted_mon& bd, const factor& b, lpvar d) {
+void order::order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const signed_vars& bd, const factor& b, lpvar d) {
     TRACE("nla_solver",  print_monomial(ac, tout << "ac=");
-          print_rooted_monomial(bd, tout << "\nrm=");
+          tout << "\nrm=" << bd;
           print_factor(b, tout << ", b="); print_var(d, tout << ", d=") << "\n";);
     int p = (k + 1) % 2;
     lpvar a = ac[p];
@@ -309,14 +304,12 @@ void order::order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const
 void order::order_lemma_on_factor_binomial_explore(const monomial& m, unsigned k) {
     SASSERT(m.size() == 2);
     lpvar c = m[k];
-    lpvar d = _().m_evars.find(c).var();
-    auto it = _().m_rm_table.var_map().find(d);
-    SASSERT(it != _().m_rm_table.var_map().end());
-    for (unsigned bd_i : it->second) {
-        order_lemma_on_factor_binomial_rm(m, k, _().m_rm_table.rms()[bd_i]);
-        if (done())
+    for (monomial const& m2 : _().m_emons.get_factors_of(c)) {
+        order_lemma_on_factor_binomial_rm(m, k, m2);
+        if (done()) {
             break;
-    }        
+        }
+    }
 }
 
 void order::order_lemma_on_binomial(const monomial& ac) {
diff --git a/src/util/lp/nla_order_lemmas.h b/src/util/lp/nla_order_lemmas.h
index b6d1c71e1..c90cd2830 100644
--- a/src/util/lp/nla_order_lemmas.h
+++ b/src/util/lp/nla_order_lemmas.h
@@ -23,29 +23,29 @@
 #include "util/lp/nla_common.h"
 
 namespace nla {
-struct core;
+class core;
 struct order: common {
     core& _() { return *m_core; }
     const core& _() const { return *m_core; }
     //constructor
     order(core *c) : common(c) {}
-    bool order_lemma_on_ac_and_bc_and_factors(const rooted_mon& ac,
+    bool order_lemma_on_ac_and_bc_and_factors(const signed_vars& ac,
                                               const factor& a,
                                               const factor& c,
-                                              const rooted_mon& bc,
+                                              const signed_vars& bc,
                                               const factor& b);
     
     // a >< b && c > 0  => ac >< bc
     // a >< b && c < 0  => ac <> bc
     // ac[k] plays the role of c   
-    bool order_lemma_on_ac_and_bc(const rooted_mon& rm_ac,
+    bool order_lemma_on_ac_and_bc(const signed_vars& rm_ac,
                                   const factorization& ac_f,
                                   unsigned k,
-                                  const rooted_mon& rm_bd);
+                                  const signed_vars& rm_bd);
     
-    bool order_lemma_on_ac_explore(const rooted_mon& rm, const factorization& ac, unsigned k);
+    bool order_lemma_on_ac_explore(const signed_vars& rm, const factorization& ac, unsigned k);
 
-    void order_lemma_on_factorization(const rooted_mon& rm, const factorization& ab);
+    void order_lemma_on_factorization(const signed_vars& rm, const factorization& ab);
     
     /**
        \brief Add lemma: 
@@ -62,20 +62,20 @@ struct order: common {
     void order_lemma_on_ab_lt(const monomial& m, const rational& sign, lpvar a, lpvar b);
     void order_lemma_on_ab(const monomial& m, const rational& sign, lpvar a, lpvar b, bool gt);
     void order_lemma_on_factor_binomial_explore(const monomial& m, unsigned k);
-    void order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const rooted_mon& rm_bd);
-    void order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const rooted_mon& bd, const factor& b, lpvar d);
+    void order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const monomial& bd);
+    void order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const signed_vars& bd, const factor& b, lpvar d);
     void order_lemma_on_binomial_k(const monomial& m, lpvar k, bool gt);
     void order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, int sign);
     void order_lemma_on_binomial(const monomial& ac);
-    void order_lemma_on_rmonomial(const rooted_mon& rm);
+    void order_lemma_on_rmonomial(const signed_vars& rm);
     void order_lemma();
     // |c_sign| = 1, and c*c_sign > 0
     // ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
-    void generate_ol(const rooted_mon& ac,                     
+    void generate_ol(const signed_vars& ac,                     
                      const factor& a,
                      int c_sign,
                      const factor& c,
-                     const rooted_mon& bc,
+                     const signed_vars& bc,
                      const factor& b,
                      llc ab_cmp);
 
@@ -83,7 +83,7 @@ struct order: common {
                          lpvar a,
                          const rational& c_sign,
                          lpvar c,
-                         const rooted_mon& bd,
+                         const signed_vars& bd,
                          const factor& b,
                          const rational& d_sign,
                          lpvar d,
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index d782dfe8d..284099c9b 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -28,8 +28,8 @@
 namespace nla {
 
 // returns the monomial index
-unsigned solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
-    return m_core->add(v, sz, vs);
+void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) {
+    m_core->add(v, sz, vs);
 }
 
 bool solver::need_check() { return true; }
diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h
index 7261f587f..a4bc4b911 100644
--- a/src/util/lp/nla_solver.h
+++ b/src/util/lp/nla_solver.h
@@ -32,8 +32,7 @@ namespace nla {
 class solver {
     core* m_core;
 public:
-    // returns the monomial index
-    unsigned add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs);
+    void add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs);
     
     solver(lp::lar_solver& s, reslimit& lim, params_ref const& p);
     ~solver();
diff --git a/src/util/lp/nla_tangent_lemmas.cpp b/src/util/lp/nla_tangent_lemmas.cpp
index 3dd6e8c65..b1f6e1ed8 100644
--- a/src/util/lp/nla_tangent_lemmas.cpp
+++ b/src/util/lp/nla_tangent_lemmas.cpp
@@ -22,7 +22,6 @@
 
 namespace nla {
 template <typename T> rational tangents::vvr(T const& t) const { return m_core->vvr(t); }
-template <typename T> lpvar tangents::var(T const& t) const { return m_core->var(t); }
 
 tangents::tangents(core * c) : common(c) {}
 std::ostream& tangents::print_point(const point &a, std::ostream& out) const {
@@ -34,13 +33,12 @@ std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std
     out << "("; print_point(a, out);  out <<  ", "; print_point(b, out); out <<  ")";
     return out;
 }
-void tangents::generate_simple_tangent_lemma(const rooted_mon* rm) {
+void tangents::generate_simple_tangent_lemma(const signed_vars* rm) {
     if (rm->size() != 2)
         return;
-    TRACE("nla_solver", tout << "rm:"; m_core->print_rooted_monomial_with_vars(*rm, tout) << std::endl;);
+    TRACE("nla_solver", tout << "rm:" << *rm << std::endl;);
     m_core->add_empty_lemma();
-    unsigned i_mon = rm->orig_index();
-    const monomial & m = c().m_monomials[i_mon];
+    const monomial & m = c().m_emons[rm->var()];
     const rational v = c().product_value(m);
     const rational& mv = vvr(m);
     SASSERT(mv != v);
@@ -58,7 +56,7 @@ void tangents::generate_simple_tangent_lemma(const rooted_mon* rm) {
             c().mk_ineq(js, j, llc::LT);
             c().mk_ineq(js, j, llc::GT, jv);
         }
-        c().mk_ineq(sign, i_mon, llc::LE, std::max(v, rational(-1)));
+        c().mk_ineq(sign, rm->var(), llc::LE, std::max(v, rational(-1)));
     } else {
         for (lpvar j : m) {
             const rational & jv = vvr(j);
@@ -75,7 +73,7 @@ void tangents::tangent_lemma() {
     bfc bf;
     lpvar j;
     rational sign;
-    const rooted_mon* rm = nullptr;
+    const signed_vars* rm = nullptr;
         
     if (c().find_bfc_to_refine(bf, j, sign, rm)) {
         tangent_lemma_bf(bf, j, sign, rm);
@@ -86,7 +84,7 @@ void tangents::tangent_lemma() {
     }
 }
 
-void tangents::generate_explanations_of_tang_lemma(const rooted_mon& rm, const bfc& bf, lp::explanation& exp) {
+void tangents::generate_explanations_of_tang_lemma(const signed_vars& rm, const bfc& bf, lp::explanation& exp) {
     // here we repeat the same explanation for each lemma
     c().explain(rm, exp);
     c().explain(bf.m_x, exp);
@@ -114,7 +112,7 @@ void tangents::generate_tang_plane(const rational & a, const rational& b, const
     t.add_coeff_var( j_sign, j);
     c().mk_ineq(t, sbelow? llc::GT : llc::LT, - a*b);
 }  
-void tangents::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const rooted_mon* rm){
+void tangents::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const signed_vars* rm){
     point a, b;
     point xy (vvr(bf.m_x), vvr(bf.m_y));
     rational correct_mult_val =  xy.x * xy.y;
diff --git a/src/util/lp/nla_tangent_lemmas.h b/src/util/lp/nla_tangent_lemmas.h
index 3ff2ae001..e4a116c9c 100644
--- a/src/util/lp/nla_tangent_lemmas.h
+++ b/src/util/lp/nla_tangent_lemmas.h
@@ -24,7 +24,7 @@
 #include "util/lp/nla_common.h"
 
 namespace nla {
-struct core;
+class core;
 struct tangents: common {   
     struct point {
         rational x;
@@ -47,13 +47,13 @@ struct tangents: common {
     
     tangents(core *core);
 
-    void generate_simple_tangent_lemma(const rooted_mon* rm);
+    void generate_simple_tangent_lemma(const signed_vars* rm);
     
     void tangent_lemma();
 
-    void generate_explanations_of_tang_lemma(const rooted_mon& rm, const bfc& bf, lp::explanation& exp);
+    void generate_explanations_of_tang_lemma(const signed_vars& rm, const bfc& bf, lp::explanation& exp);
     
-    void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const rooted_mon* rm);
+    void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const signed_vars* rm);
     void generate_tang_plane(const rational & a, const rational& b, const factor& x, const factor& y, bool below, lpvar j, const rational& j_sign);
     
     void generate_two_tang_lines(const bfc & bf, const point& xy, const rational& sign, lpvar j);
@@ -76,6 +76,6 @@ struct tangents: common {
                                const rational & val,
                                bool below) const;
     template <typename T> rational vvr(T const& t) const;
-    template <typename T> lpvar var(T const& t) const;
+    template <typename T> lpvar var(T const& t) const { return t.var(); }
 }; // end of tangents
 }