diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp
index a2129323b..f5bbc1832 100644
--- a/src/util/lp/emonomials.cpp
+++ b/src/util/lp/emonomials.cpp
@@ -28,7 +28,7 @@ namespace nla {
     void emonomials::inc_visited() const {
         ++m_visited;
         if (m_visited == 0) {
-            for (auto& svt : m_canonized) {
+            for (auto& svt : m_monomials) {
                 svt.visited() = 0;
             }
             ++m_visited;
@@ -45,7 +45,7 @@ namespace nla {
         m_ve.pop(n);
         unsigned old_sz = m_lim[m_lim.size() - n];
         for (unsigned i = m_monomials.size(); i-- > old_sz; ) {
-            monomial const& m = m_monomials[i];
+            monomial & m = m_monomials[i];
             remove_cg(i, m);
             m_var2index[m.var()] = UINT_MAX;
             lpvar last_var = UINT_MAX;
@@ -57,7 +57,7 @@ namespace nla {
             }
         }
         m_monomials.shrink(old_sz);
-        m_canonized.shrink(old_sz);
+        m_monomials.shrink(old_sz);
         m_region.pop_scope(n);
         m_lim.shrink(m_lim.size() - n);
     }
@@ -132,7 +132,7 @@ namespace nla {
         return m_use_lists[v].m_head;
     }
 
-    smon const* emonomials::find_canonical(svector<lpvar> const& vars) const {
+    monomial const* emonomials::find_canonical(svector<lpvar> const& vars) const {
         SASSERT(m_ve.is_root(vars));
         // find a unique key for dummy monomial
         lpvar v = m_var2index.size();
@@ -143,19 +143,17 @@ namespace nla {
             }
         }
         unsigned idx = m_monomials.size();
-        m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr()));
-        m_canonized.push_back(smon(v, idx));
+        m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr(), idx));
         m_var2index.setx(v, idx, UINT_MAX);
         do_canonize(m_monomials[idx]);
-        smon const* result = nullptr;
+        monomial const* result = nullptr;
         lpvar w; 
         if (m_cg_table.find(v, w)) {
             SASSERT(w != v);
-            result = &m_canonized[m_var2index[w]];
+            result = &m_monomials[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;
     }
 
@@ -170,7 +168,7 @@ namespace nla {
         do {
             unsigned idx = c->m_index;
             c = c->m_next;
-            monomial const& m = m_monomials[idx];
+            monomial & m = m_monomials[idx];
             if (!is_visited(m)) {
                 set_visited(m);
                 remove_cg(idx, m);
@@ -179,8 +177,8 @@ namespace nla {
         while (c != first);
     }
 
-    void emonomials::remove_cg(unsigned idx, monomial const& m) {
-        smon& sv = m_canonized[idx];
+    void emonomials::remove_cg(unsigned idx, monomial& m) {
+        monomial& sv = m_monomials[idx];
         unsigned next = sv.next();
         unsigned prev = sv.prev();
         
@@ -194,8 +192,8 @@ namespace nla {
             }
         }
         if (prev != idx) {
-            m_canonized[next].prev() = prev;
-            m_canonized[prev].next() = next;
+            m_monomials[next].prev() = prev;
+            m_monomials[prev].next() = next;
             sv.next() = idx;
             sv.prev() = idx;
         }
@@ -204,7 +202,7 @@ namespace nla {
     /**
        \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 (smon) are considered
+       variable equivalences. The canonized monomials (monomial) are considered
        in the same equivalence class if they have the same set of representative
        variables. Their signs may differ.       
     */
@@ -219,7 +217,7 @@ namespace nla {
         do {
             unsigned idx = c->m_index;
             c = c->m_next;
-            monomial const& m = m_monomials[idx];
+            monomial & m = m_monomials[idx];
             if (!is_visited(m)) {
                 set_visited(m);
                 insert_cg(idx, m);
@@ -228,31 +226,31 @@ namespace nla {
         while (c != first);
     }
 
-    void emonomials::insert_cg(unsigned idx, monomial const& m) {
+    void emonomials::insert_cg(unsigned idx, monomial & m) {
         do_canonize(m);
         lpvar v = m.var(), w;
         if (m_cg_table.find(v, w)) {
             SASSERT(w != v);
             unsigned idxr = m_var2index[w];
-            unsigned idxl = m_canonized[idxr].prev();
-            m_canonized[idx].next()  = idxr;
-            m_canonized[idx].prev()  = idxl;
-            m_canonized[idxr].prev() = idx;
-            m_canonized[idxl].next() = idx;
+            unsigned idxl = m_monomials[idxr].prev();
+            m_monomials[idx].next()  = idxr;
+            m_monomials[idx].prev()  = idxl;
+            m_monomials[idxr].prev() = idx;
+            m_monomials[idxl].next() = idx;
         }
         else {
             m_cg_table.insert(v);
-            SASSERT(m_canonized[idx].next() == idx);
-            SASSERT(m_canonized[idx].prev() == idx);
+            SASSERT(m_monomials[idx].next() == idx);
+            SASSERT(m_monomials[idx].prev() == idx);
         }        
     }
 
-    void emonomials::set_visited(monomial const& m) const {
-        m_canonized[m_var2index[m.var()]].visited() = m_visited;
+    void emonomials::set_visited(monomial& m) const {
+        m_monomials[m_var2index[m.var()]].visited() = m_visited;
     }
 
     bool emonomials::is_visited(monomial const& m) const {
-        return m_visited == m_canonized[m_var2index[m.var()]].visited();
+        return m_visited == m_monomials[m_var2index[m.var()]].visited();
     }
 
     /**
@@ -264,8 +262,7 @@ namespace nla {
      */
     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(smon(v, idx));
+        m_monomials.push_back(monomial(v, sz, vs, idx));
         lpvar last_var = UINT_MAX;
         for (unsigned i = 0; i < sz; ++i) {
             lpvar w = vs[i];
@@ -281,33 +278,29 @@ namespace nla {
         insert_cg(idx, m_monomials[idx]);
     }
 
-    void emonomials::do_canonize(monomial const& mon) const {
-        unsigned index = m_var2index[mon.var()];
-        smon& svs = m_canonized[index];
-        svs.reset();
-        for (lpvar v : mon) {
-            svs.push_var(m_ve.find(v));
+    void emonomials::do_canonize(monomial & m) const {
+        m.reset_rfields();
+        for (lpvar v : m.vars()) {
+            m.push_rvar(m_ve.find(v));
         }
-        svs.done_push();
+        m.sort_rvars();
     }
 
-    bool emonomials::canonize_divides(monomial const& m1, monomial const& m2) const {
-        if (m1.size() > m2.size()) return false;
-        smon const& s1 = canonize(m1);
-        smon const& s2 = canonize(m2);
-        unsigned sz1 = s1.size(), sz2 = s2.size();
+    bool emonomials::canonize_divides(monomial& m, monomial & n) const {
+        if (m.size() > n.size()) return false;
+        unsigned ms = m.size(), ns = n.size();
         unsigned i = 0, j = 0;
         while (true) {
-            if (i == sz1) {
+            if (i == ms) {
                 return true;
             }
-            else if (j == sz2) {
+            else if (j == ns) {
                 return false;
             }
-            else if (s1[i] == s2[j]) {
+            else if (m.rvars()[i] == n.rvars()[j]) {
                 ++i; ++j;
             }
-            else if (s1[i] < s2[j]) {
+            else if (m.rvars()[i] < n.rvars()[j]) {
                 return false;
             }
             else {
@@ -316,16 +309,9 @@ namespace nla {
         }
     }
 
-    void emonomials::explain_canonized(monomial const& m, lp::explanation& exp) {
-        for (lpvar v : m) {
-            signed_var w = m_ve.find(v);
-            m_ve.explain(signed_var(v, false), w, exp);
-        }
-    }
-
-    // yes, assume that monomials are non-empty.
-    emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial const& mon, bool at_end):
-        m(m), m_mon(&mon), m_it(iterator(m, m.head(mon[0]), at_end)), m_end(iterator(m, m.head(mon[0]), true)) {
+// yes, assume that monomials are non-empty.
+    emonomials::pf_iterator::pf_iterator(emonomials const& m, monomial & mon, bool at_end):
+        m(m), m_mon(&mon), m_it(iterator(m, m.head(mon.vars()[0]), at_end)), m_end(iterator(m, m.head(mon.vars()[0]), true)) {
         fast_forward();
     }
 
diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h
index ea16091fe..7d638c8e7 100644
--- a/src/util/lp/emonomials.h
+++ b/src/util/lp/emonomials.h
@@ -27,51 +27,6 @@
 
 namespace nla {
 
-    /**
-       \brief class used to summarize the coefficients to a monomial after
-       canonization with respect to current equalities.
-    */
-class smon  {
-    lpvar           m_var; // variable representing original monomial
-    svector<lpvar>  m_rvars;
-    bool            m_rsign;
-    unsigned m_next;                    // next congruent node.
-    unsigned m_prev;                    // previous congruent node
-    mutable unsigned m_visited;
-public:
-    smon(lpvar v, unsigned idx): m_var(v), m_rsign(false), m_next(idx), m_prev(idx), m_visited(0) {}
-            lpvar var() const { return m_var; }
-    unsigned next() const { return m_next; }
-    unsigned& next() { return m_next; }
-    unsigned prev() const { return m_prev; }
-    unsigned& prev() { return m_prev; }
-    unsigned visited() const { return m_visited; }
-    unsigned& visited() { return m_visited; }
-    svector<lpvar> const& rvars() const { return m_rvars; }
-    svector<lp::var_index>::const_iterator begin() const { return rvars().begin(); }
-    svector<lp::var_index>::const_iterator end() const { return rvars().end(); }
-    unsigned size() const { return m_rvars.size(); }
-    lpvar operator[](unsigned i) const { return m_rvars[i]; }
-    bool sign() const { return m_rsign; }
-    rational rsign() const { return rational(m_rsign ? -1 : 1); }
-    void reset() { m_rsign = false; m_rvars.reset(); }
-    void push_var(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); }
-    void done_push() {
-        std::sort(m_rvars.begin(), m_rvars.end());
-    }
-    std::ostream& display(std::ostream& out) const {
-        // out << "v" << var() << " := ";
-        // if (sign()) out << "- ";
-        // for (lpvar v : vars()) out << "v" << v << " ";
-        SASSERT(false);
-        return out;
-    }
-
-};
-
-inline std::ostream& operator<<(std::ostream& out, smon const& m) { return m.display(out); }
-
-
 class emonomials : public var_eqs_merge_handler {
 
     /**
@@ -97,7 +52,7 @@ class emonomials : public var_eqs_merge_handler {
         hash_canonical(emonomials& em): em(em) {}
             
         unsigned operator()(lpvar v) const {
-            auto const& vec = em.m_canonized[em.m_var2index[v]].rvars();
+            auto const& vec = em.m_monomials[em.m_var2index[v]].rvars();
             return string_hash(reinterpret_cast<char const*>(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10);
         }
     };
@@ -112,8 +67,8 @@ class emonomials : public var_eqs_merge_handler {
         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]].rvars();
-            auto const& vvec = em.m_canonized[em.m_var2index[v]].rvars();
+            auto const& uvec = em.m_monomials[em.m_var2index[u]].rvars();
+            auto const& vvec = em.m_monomials[em.m_var2index[v]].rvars();
             return uvec == vvec;
         }
     };
@@ -124,7 +79,6 @@ class emonomials : public var_eqs_merge_handler {
     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<smon>  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;
@@ -139,16 +93,16 @@ class emonomials : public var_eqs_merge_handler {
 
     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 insert_cg(unsigned idx, monomial & m);
+    void remove_cg(unsigned idx, monomial & m);
     void rehash_cg(lpvar v) { remove_cg(v); insert_cg(v); }
 
-    void do_canonize(monomial const& m) const; 
+    void do_canonize(monomial& m) const; 
 
     cell* head(lpvar v) const;
-    void set_visited(monomial const& m) const;
+    void set_visited(monomial& m) const;
     bool is_visited(monomial const& m) const;
-        
+     
 public:
     /**
        \brief emonomials builds on top of var_eqs.
@@ -160,8 +114,7 @@ public:
         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_cg_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_cg_hash, m_cg_eq) { 
         m_ve.set_merge_handler(this); 
     }
 
@@ -184,59 +137,23 @@ public:
     /**
        \brief retrieve monomial corresponding to variable v from definition v := vs
     */
-    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); }
-
-    monomial const& operator[](smon const& m) const { return var2monomial(m.var()); }
-
-    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
-    */
-    smon const& var2canonical(lpvar v) const { return canonize(var2monomial(v)); }
-        
-    class canonical {
-        emonomials& m;
-    public:
-        canonical(emonomials& m): m(m) {}
-        smon const& operator[](lpvar v) const { return m.var2canonical(v); }
-        smon const& operator[](monomial const& mon) const { return m.var2canonical(mon.var()); }
-    };
-
-    canonical canonical;
-        
-    /**
-       \brief obtain a canonized signed monomial
-       corresponding to current equivalence class.
-    */
-    smon const& canonize(monomial const& m) const { return m_canonized[m_var2index[m.var()]]; }
-
+    monomial const& operator[](lpvar v) const { return m_monomials[m_var2index[v]]; }
+    monomial & operator[](lpvar v) { return m_monomials[m_var2index[v]]; }
+                                                                           
     /**
        \brief obtain the representative canonized monomial up to sign.
     */
-    //smon const& rep(smon const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
-    smon const& rep(smon const& sv) const {
+
+    monomial const& rep(monomial const& sv) const {
         unsigned j = -1;
         m_cg_table.find(sv.var(), j);
-        return m_canonized[m_var2index[j]];
+        return m_monomials[m_var2index[j]];
     }
 
-    /**
-       \brief the original sign is defined as a sign of the equivalence class representative.
-    */
-    rational orig_sign(smon const& sv) const { return rep(sv).rsign(); }           
-
     /**
        \brief determine if m1 divides m2 over the canonization obtained from merged variables.
     */
-    bool canonize_divides(monomial const& m1, monomial const& m2) const;
-
-    /**
-       \brief produce explanation for monomial canonization.
-    */
-    void explain_canonized(monomial const& m, lp::explanation& exp);
+    bool canonize_divides(monomial & m1, monomial& m2) const;
 
     /**
        \brief iterator over monomials that are declared.
@@ -253,7 +170,7 @@ public:
         bool        m_touched;            
     public:
         iterator(emonomials const& m, cell* c, bool at_end): m(m), m_cell(c), m_touched(at_end || c == nullptr) {}
-        monomial const& operator*() { return m.m_monomials[m_cell->m_index]; }
+        monomial & operator*() { return m.m_monomials[m_cell->m_index]; }
         iterator& operator++() { m_touched = true; m_cell = m_cell->m_next; return *this; }
         iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
         bool operator==(iterator const& other) const { return m_cell == other.m_cell && m_touched == other.m_touched; }
@@ -277,15 +194,15 @@ public:
     */
     class pf_iterator {
         emonomials const& m;
-        monomial const*   m_mon; // monomial
+        monomial *   m_mon; // monomial
         iterator          m_it;  // iterator over the first variable occurs list, ++ filters out elements that are not factors.
         iterator          m_end;
 
         void fast_forward();
     public:
-        pf_iterator(emonomials const& m, monomial const& mon, bool at_end);
+        pf_iterator(emonomials const& m, monomial& mon, bool at_end);
         pf_iterator(emonomials const& m, lpvar v, bool at_end);
-        monomial const& operator*() { return *m_it; }
+        monomial & operator*() { return *m_it; }
         pf_iterator& operator++() { ++m_it; fast_forward(); return *this; }
         pf_iterator operator++(int) { pf_iterator tmp = *this; ++*this; return tmp; }
         bool operator==(pf_iterator const& other) const { return m_it == other.m_it; }
@@ -294,19 +211,19 @@ public:
 
     class factors_of {
         emonomials const& m;
-        monomial const* mon;
+        monomial * mon;
         lpvar           m_var;
     public:
-        factors_of(emonomials const& m, monomial const& mon): m(m), mon(&mon), m_var(UINT_MAX) {}
+        factors_of(emonomials const& m, monomial & mon): m(m), mon(&mon), m_var(UINT_MAX) {}
         factors_of(emonomials const& m, lpvar v): m(m), mon(nullptr), m_var(v) {}
         pf_iterator begin() { if (mon) return pf_iterator(m, *mon, false); return pf_iterator(m, m_var, false); }
         pf_iterator end() { if (mon) return pf_iterator(m, *mon, true); return pf_iterator(m, m_var, true); }
     };
 
-    factors_of get_factors_of(monomial const& m) const { inc_visited(); return factors_of(*this, m); }
+    factors_of get_factors_of(monomial& m) const { inc_visited(); return factors_of(*this, m); }
     factors_of get_factors_of(lpvar v) const { inc_visited(); return factors_of(*this, v); }
        
-    smon const* find_canonical(svector<lpvar> const& vars) const;
+    monomial const* find_canonical(svector<lpvar> const& vars) const;
 
     /**
        \brief iterator over sign equivalent monomials.
@@ -324,7 +241,7 @@ public:
 
         sign_equiv_monomials_it& operator++() { 
             m_touched = true; 
-            m_index = m.m_canonized[m_index].next(); 
+            m_index = m.m_monomials[m_index].next(); 
             return *this; 
         }
 
@@ -355,8 +272,6 @@ public:
 
     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(smon const& sv) { return enum_sign_equiv_monomials(sv.var()); }
-
     /**
        \brief display state of emonomials
     */
@@ -373,6 +288,7 @@ public:
 
     void unmerge_eh(signed_var r2, signed_var r1) override;        
 
+    bool is_monomial_var(lpvar v) const { return m_var2index.get(v, UINT_MAX) != UINT_MAX; }
 };
 
 inline std::ostream& operator<<(std::ostream& out, emonomials const& m) { return m.display(out); }
diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h
index ff6908113..bbc4c4e7f 100644
--- a/src/util/lp/factorization.h
+++ b/src/util/lp/factorization.h
@@ -54,7 +54,7 @@ class factorization {
 public:
     factorization(const monomial* m): m_mon(m) {
         if (m != nullptr) {
-            for (lpvar j : *m)
+            for (lpvar j : m->vars())
                 m_vars.push_back(factor(j, factor_type::VAR));
         }
     }
diff --git a/src/util/lp/factorization_factory_imp.cpp b/src/util/lp/factorization_factory_imp.cpp
index a1ef6edc7..0228eaa2a 100644
--- a/src/util/lp/factorization_factory_imp.cpp
+++ b/src/util/lp/factorization_factory_imp.cpp
@@ -21,7 +21,7 @@
 #include "util/lp/nla_core.h"
 namespace nla {
         
-factorization_factory_imp::factorization_factory_imp(const smon& rm, const core& s) :
+factorization_factory_imp::factorization_factory_imp(const monomial& rm, const core& s) :
     factorization_factory(rm.rvars(), &s.m_emons[rm.var()]),
     m_core(s), m_mon(s.m_emons[rm.var()]), m_rm(rm) { }
         
diff --git a/src/util/lp/factorization_factory_imp.h b/src/util/lp/factorization_factory_imp.h
index 5f674026d..ae1c8d9a0 100644
--- a/src/util/lp/factorization_factory_imp.h
+++ b/src/util/lp/factorization_factory_imp.h
@@ -21,14 +21,13 @@
 #include "util/lp/factorization.h"
 namespace nla {
     class  core;
-    class smon;
 
     struct factorization_factory_imp: factorization_factory {
         const core&  m_core;
         const monomial & m_mon;
-        const smon& m_rm;
+        const monomial& m_rm;
         
-        factorization_factory_imp(const smon& rm, const core& s);
+        factorization_factory_imp(const monomial& 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/mon_eq.cpp b/src/util/lp/mon_eq.cpp
index dc11a5be9..07a1b7577 100644
--- a/src/util/lp/mon_eq.cpp
+++ b/src/util/lp/mon_eq.cpp
@@ -5,24 +5,25 @@
 #include "util/lp/lar_solver.h"
 #include "util/lp/monomial.h"
 namespace nla {
-typedef monomial mon_eq;
-bool check_assignment(mon_eq const& m, variable_map_type & vars) {
+
+template <typename T>
+bool check_assignment(T const& m, variable_map_type & vars) {
     rational r1 = vars[m.var()];
     if (r1.is_zero()) {
-        for (auto w : m) {
+        for (auto w : m.vars()) {
             if (vars[w].is_zero())
                 return true;
         }
         return false;
     }
     rational r2(1);
-    for (auto w : m) {
+    for (auto w : m.vars()) {
         r2 *= vars[w];
     }
     return r1 == r2;
 }
-
-bool check_assignments(const vector<mon_eq> & monomials,
+template <typename K>
+bool check_assignments(const K & monomials,
                        const lp::lar_solver& s,
                        variable_map_type & vars) {
     s.get_model(vars);
@@ -32,4 +33,8 @@ bool check_assignments(const vector<mon_eq> & monomials,
     return true;
 }
 
+template bool check_assignments<vector<mon_eq>>(const vector<mon_eq>&,
+                                            const lp::lar_solver& s,
+                                            variable_map_type & vars);
+
 }
diff --git a/src/util/lp/monomial.h b/src/util/lp/monomial.h
index 321c24000..15cdf9499 100644
--- a/src/util/lp/monomial.h
+++ b/src/util/lp/monomial.h
@@ -8,72 +8,86 @@
 #include "util/lp/lp_settings.h"
 #include "util/vector.h"
 #include "util/lp/lar_solver.h"
-
+#include "util/lp/nla_defs.h"
 namespace nla {
 /*
  *  represents definition m_v = v1*v2*...*vn, 
  *  where m_vs = [v1, v2, .., vn]
  */
-class monomial {
+
+class mon_eq {
     // fields
     lp::var_index          m_v;
     svector<lp::var_index> m_vs;
 public:
     // constructors
-    monomial(lp::var_index v, unsigned sz, lp::var_index const* vs):
+    mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs):
         m_v(v), m_vs(sz, vs) {
         std::sort(m_vs.begin(), m_vs.end());
     }
-    monomial(lp::var_index v, const svector<lp::var_index> &vs):
+    mon_eq(lp::var_index v, const svector<lp::var_index> &vs):
         m_v(v), m_vs(vs) {
         std::sort(m_vs.begin(), m_vs.end());
     }
-    monomial() {}
+    mon_eq() {}
         
     unsigned var() const { return m_v; }
     unsigned size() const { return m_vs.size(); }
-    unsigned operator[](unsigned idx) const { return m_vs[idx]; }
-    svector<lp::var_index>::const_iterator begin() const { return m_vs.begin(); }
-    svector<lp::var_index>::const_iterator end() const { return m_vs.end(); }
     const svector<lp::var_index>& vars() const { return m_vs; }
+    svector<lp::var_index>& vars() { return m_vs; }
     bool empty() const { return m_vs.empty(); }
+};
 
-        std::ostream& display(std::ostream& out) const {
-            out << "v" << var() << " := ";
-            for (auto v : *this) {
-                out << "v" << v << " ";
-            }
-            return out;
-        }
-    };
-
-    inline std::ostream& operator<<(std::ostream& out, monomial const& m) {
-        SASSERT(false);
-        return m.display(out);
+// support the congruence    
+class monomial: public mon_eq {
+    // fields
+    svector<lpvar>  m_rvars;
+    bool            m_rsign;
+    unsigned         m_next;                    // next congruent node.
+    unsigned         m_prev;                    // previous congruent node
+    mutable unsigned m_visited;
+public:
+    // constructors
+    monomial(lpvar v, unsigned sz, lpvar const* vs, unsigned idx):  monomial(v, svector<lpvar>(sz, vs), idx) {
+    }
+    monomial(lpvar v, const svector<lpvar> &vs, unsigned idx) : mon_eq(v, vs), m_rsign(false), m_next(idx), m_prev(idx), m_visited(0) {
+        std::sort(vars().begin(), vars().end());
     }
 
-    typedef std::unordered_map<lp::var_index, rational> variable_map_type;
-    
-bool check_assignment(monomial const& m, variable_map_type & vars);
-    
-bool check_assignments(const vector<monomial> & monomimials,
+    unsigned next() const { return m_next; }
+    unsigned& next() { return m_next; }
+    unsigned prev() const { return m_prev; }
+    unsigned& prev() { return m_prev; }
+    unsigned visited() const { return m_visited; }
+    unsigned& visited() { return m_visited; }
+    svector<lpvar> const& rvars() const { return m_rvars; }
+    bool sign() const { return m_rsign; }
+    rational rsign() const { return rational(m_rsign ? -1 : 1); }
+    void reset_rfields() { m_rsign = false; m_rvars.reset(); }
+    void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); }
+    void sort_rvars() {
+        std::sort(m_rvars.begin(), m_rvars.end());
+    }
+    std::ostream& display(std::ostream& out) const {
+        // out << "v" << var() << " := ";
+        // if (sign()) out << "- ";
+        // for (lpvar v : vars()) out << "v" << v << " ";
+        SASSERT(false);
+        return out;
+    }
+};
+
+inline std::ostream& operator<<(std::ostream& out, monomial const& m) {
+    SASSERT(false);
+    return m.display(out);
+}
+
+typedef std::unordered_map<lpvar, rational> variable_map_type;
+template <typename T>
+bool check_assignment(T const& m, variable_map_type & vars);
+template <typename K>
+bool check_assignments(const K & monomimials,
                        const lp::lar_solver& s,
                        variable_map_type & vars);
 
-
-
-    /*
-     *  represents definition m_v = coeff* v1*v2*...*vn, 
-     *  where m_vs = [v1, v2, .., vn]
-     */
-    class monomial_coeff  {
-        svector<lp::var_index> m_vs;
-        rational m_coeff;
-    public:
-        monomial_coeff(const svector<lp::var_index>& vs, rational const& coeff): m_vs(vs), m_coeff(coeff) {}
-
-        rational const& coeff() const { return m_coeff; }
-        const svector<lp::var_index> & vars() const { return m_vs; } 
-    };
-
-}
+} // end of namespace nla
diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp
index 925948e4a..b3270754c 100644
--- a/src/util/lp/nla_basics_lemmas.cpp
+++ b/src/util/lp/nla_basics_lemmas.cpp
@@ -26,8 +26,9 @@ 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)
+bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n) {
+    const rational& sign = m.rsign() * n.rsign();
+     if (vvr(m) == vvr(n) * sign)
         return false;
     TRACE("nla_solver", tout << "sign contradiction:\nm = " << m << "n= " << n << "sign: " << sign << "\n";);
     generate_sign_lemma(m, n, sign);
@@ -35,13 +36,13 @@ bool basics::basic_sign_lemma_on_two_monomials(const monomial& m, const monomial
 }
 
 void basics::generate_zero_lemmas(const monomial& m) {
-    SASSERT(!vvr(m).is_zero() && c().product_value(m).is_zero());
+    SASSERT(!vvr(m).is_zero() && c().product_value(m.vars()).is_zero());
     int sign = nla::rat_sign(vvr(m));
     unsigned_vector fixed_zeros;
     lpvar zero_j = find_best_zero(m, fixed_zeros);
     SASSERT(is_set(zero_j));
     unsigned zero_power = 0;
-    for (lpvar j : m){
+    for (lpvar j : m.vars()){
         if (j == zero_j) {
             zero_power++;
             continue;
@@ -91,7 +92,7 @@ void basics::basic_sign_lemma_model_based_one_mon(const monomial& m, int product
         generate_zero_lemmas(m);
     } else {
         add_empty_lemma();
-        for(lpvar j: m) {
+        for(lpvar j: m.vars()) {
             negate_strict_sign(j);
         }
         c().mk_ineq(m.var(), product_sign == 1? llc::GT : llc::LT);
@@ -122,12 +123,10 @@ bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set<unsigned> & exp
     }
 
     const monomial& m_v = c().m_emons[v];
-    smon const& sv_v = c().m_emons.canonical[v];
     TRACE("nla_solver_details", tout << "mon = " << pp_mon(c(), m_v););
 
-    for (auto const& m_w : c().m_emons.enum_sign_equiv_monomials(v)) {
-        smon 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()) 
+    for (auto const& m : c().m_emons.enum_sign_equiv_monomials(v)) {
+        if (m_v.var() != m.var() && basic_sign_lemma_on_two_monomials(m_v, m) && done()) 
             return true;
     }
 
@@ -167,7 +166,7 @@ void basics::generate_sign_lemma(const monomial& m, const monomial& n, const rat
 // and the bounds on j contain 0 as an inner point
 lpvar basics::find_best_zero(const monomial& m, unsigned_vector & fixed_zeros) const {
     lpvar zero_j = -1;
-    for (unsigned j : m){
+    for (unsigned j : m.vars()){
         if (vvr(j).is_zero()){
             if (c().var_is_fixed_to_zero(j))
                 fixed_zeros.push_back(j);
@@ -189,7 +188,7 @@ void basics::generate_strict_case_zero_lemma(const monomial& m, unsigned zero_j,
     // we know all the signs
     add_empty_lemma();
     c().mk_ineq(zero_j, (sign_of_zj == 1? llc::GT : llc::LT));
-    for (unsigned j : m){
+    for (unsigned j : m.rvars()){
         if (j != zero_j) {
             negate_strict_sign(j);
         }
@@ -222,7 +221,7 @@ 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 smon& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_zero(const monomial& rm, const factorization& f) {
     NOT_IMPLEMENTED_YET();
     return true;
 #if 0
@@ -251,7 +250,7 @@ bool basics::basic_lemma(bool derived) {
     unsigned sz = rm_ref.size();
     for (unsigned j = 0; j < sz; ++j) {
         lpvar v = rm_ref[(j + start) % rm_ref.size()];
-        const smon& r = c().m_emons.canonical[v];
+        const monomial& r = c().m_emons[v];
         SASSERT (!c().check_monomial(c().m_emons[v]));
         basic_lemma_for_mon(r, derived);
     } 
@@ -261,13 +260,13 @@ bool basics::basic_lemma(bool derived) {
 // 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 smon& rm, bool derived) {
+void basics::basic_lemma_for_mon(const monomial& 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 smon& rm) {
+bool basics::basic_lemma_for_mon_derived(const monomial& rm) {
     if (c().var_is_fixed_to_zero(var(rm))) {
         for (auto factorization : factorization_factory_imp(rm, c())) {
             if (factorization.is_empty())
@@ -293,7 +292,7 @@ bool basics::basic_lemma_for_mon_derived(const smon& rm) {
     return false;
 }
 // x = 0 or y = 0 -> xy = 0
-bool basics::basic_lemma_for_mon_non_zero_derived(const smon& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_non_zero_derived(const monomial& 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; 
@@ -317,7 +316,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const smon& rm, const factoriz
 }
 // 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 smon& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomial& rm, const factorization& f) {
     TRACE("nla_solver",  c().trace_print_monomial_and_factorization(rm, f, tout););
 
     lpvar mon_var =  c().m_emons[rm.var()].var();
@@ -375,64 +374,14 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const smon&
     TRACE("nla_solver",  c().print_lemma(tout); );
     return true;
 }
-// use the fact
-// 1 * 1 ... * 1 * x * 1 ... * 1 = x
-bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const smon& rm, const factorization& f) {
-    return false;
-    rational sign = c().m_emons.orig_sign(rm);
-    lpvar not_one = -1;
 
-    TRACE("nla_solver", tout << "f = ";  c().print_factorization(f, tout););
-    for (auto j : f){
-        TRACE("nla_solver", tout << "j = ";  c().print_factor_with_vars(j, tout););
-        auto v = vvr(j);
-        if (v == rational(1)) {
-            continue;
-        }
-
-        if (v == -rational(1)) { 
-            sign = - sign;
-            continue;
-        } 
-
-        if (not_one == static_cast<lpvar>(-1)) {
-            not_one = var(j);
-            continue;
-        }
-
-        // if we are here then there are at least two factors with values different from one and minus one: cannot create the lemma
-        return false;
-    }
-
-    add_empty_lemma();
-    explain(rm);
-
-    for (auto j : f){
-        lpvar var_j = var(j);
-        if (not_one == var_j) continue;
-        c().mk_ineq(var_j, llc::NE, j.is_var()? vvr(j) :  c().canonize_sign(j) * vvr(j));   
-    }
-
-    if (not_one == static_cast<lpvar>(-1)) {
-        c().mk_ineq( c().m_emons[rm.var()].var(), llc::EQ, sign);
-    } else {
-        c().mk_ineq( c().m_emons[rm.var()].var(), -sign, not_one, llc::EQ);
-    }
-    TRACE("nla_solver",
-          tout << "rm = " << rm;
-          c().print_lemma(tout););
-    return true;
-}
-
-bool basics::basic_lemma_for_mon_neutral_derived(const smon& rm, const factorization& factorization) {
+bool basics::basic_lemma_for_mon_neutral_derived(const monomial& 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);
-    return false;
+        basic_lemma_for_mon_neutral_monomial_to_factor_derived(rm, factorization);
 }
 
 // x != 0 or y = 0 => |xy| >= |y|
-void basics::proportion_lemma_model_based(const smon& rm, const factorization& factorization) {
+void basics::proportion_lemma_model_based(const monomial& rm, const factorization& factorization) {
     rational rmv = abs(vvr(rm));
     if (rmv.is_zero()) {
         SASSERT(c().has_zero_factor(factorization));
@@ -448,7 +397,7 @@ void basics::proportion_lemma_model_based(const smon& rm, const factorization& f
     }
 }
 // x != 0 or y = 0 => |xy| >= |y|
-bool basics::proportion_lemma_derived(const smon& rm, const factorization& factorization) {
+bool basics::proportion_lemma_derived(const monomial& rm, const factorization& factorization) {
     return false;
     rational rmv = abs(vvr(rm));
     if (rmv.is_zero()) {
@@ -473,7 +422,7 @@ void basics::generate_pl_on_mon(const monomial& m, unsigned factor_index) {
     rational sm = rational(nla::rat_sign(mv));
     c().mk_ineq(sm, mon_var, llc::LT);
     for (unsigned fi = 0; fi < m.size(); fi ++) {
-        lpvar j = m[fi];
+        lpvar j = m.vars()[fi];
         if (fi != factor_index) {
             c().mk_ineq(j, llc::EQ);
         } else {
@@ -489,10 +438,10 @@ 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 smon& rm, const factorization& fc, int factor_index) {
-    TRACE("nla_solver", tout << "factor_index = " << factor_index << ", rm = ";
-          tout << rm;
-          tout << "fc = "; c().print_factorization(fc, tout);
+void basics::generate_pl(const monomial& rm, const factorization& fc, int factor_index) {
+    TRACE("nla_solver", tout << "factor_index = " << factor_index << ", rm = "
+          << pp_mon(c(), rm);
+          tout << ", fc = "; c().print_factorization(fc, 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);
@@ -523,7 +472,7 @@ void basics::generate_pl(const smon& rm, const factorization& fc, int factor_ind
     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 smon& rm, const factorization& f) {        
+void basics::basic_lemma_for_mon_zero_model_based(const monomial& 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();
@@ -544,7 +493,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const smon& rm, const factoriz
     TRACE("nla_solver", c().print_lemma(tout););
 }
 
-void basics::basic_lemma_for_mon_model_based(const smon& rm) {
+void basics::basic_lemma_for_mon_model_based(const monomial& rm) {
     TRACE("nla_solver_bl", tout << "rm = " << rm;);
     if (vvr(rm).is_zero()) {
         for (auto factorization : factorization_factory_imp(rm, c())) {
@@ -576,7 +525,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
         return false;
     }
     lpvar jl = -1;
-    for (auto j : m ) {
+    for (auto j : m.vars() ) {
         if (abs(vvr(j)) == abs_mv) {
             jl = j;
             break;
@@ -585,7 +534,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based_fm(const
     if (jl == static_cast<lpvar>(-1))
         return false;
     lpvar not_one_j = -1;
-    for (auto j : m ) {
+    for (auto j : m.vars() ) {
         if (j == jl) {
             continue;
         }
@@ -623,7 +572,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
     lpvar not_one = -1;
     rational sign(1);
     TRACE("nla_solver_bl", tout << "m = "; c().print_monomial(m, tout););
-    for (auto j : m){
+    for (auto j : m.vars()){
         auto v = vvr(j);
         if (v == rational(1)) {
             continue;
@@ -648,7 +597,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based_fm
     }
         
     add_empty_lemma();
-    for (auto j : m){
+    for (auto j : m.vars()){
         if (not_one == j) continue;
         c().mk_ineq(j, llc::NE, vvr(j));   
     }
@@ -664,7 +613,7 @@ 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 smon& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const monomial& rm, const factorization& f) {
     TRACE("nla_solver_bl", c().trace_print_monomial_and_factorization(rm, f, tout););
 
     lpvar mon_var = c().m_emons[rm.var()].var();
@@ -722,7 +671,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const sm
     return true;
 }
 
-void basics::basic_lemma_for_mon_neutral_model_based(const smon& rm, const factorization& f) {
+void basics::basic_lemma_for_mon_neutral_model_based(const monomial& 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());
@@ -734,8 +683,8 @@ void basics::basic_lemma_for_mon_neutral_model_based(const smon& rm, const facto
 }
 // use the fact
 // 1 * 1 ... * 1 * x * 1 ... * 1 = x
-bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const smon& rm, const factorization& f) {
-    rational sign = c().m_emons.orig_sign(rm);
+bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const monomial& rm, const factorization& f) {
+    rational sign = rm.rsign();
     TRACE("nla_solver_bl", tout << "f = "; c().print_factorization(f, tout); tout << ", sign = " << sign << '\n'; );
     lpvar not_one = -1;
     for (auto j : f){
@@ -815,7 +764,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 smon& rm, const factorization& f) {
+void basics::basic_lemma_for_mon_non_zero_model_based(const monomial& 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 494e5b8ca..12e32153a 100644
--- a/src/util/lp/nla_basics_lemmas.h
+++ b/src/util/lp/nla_basics_lemmas.h
@@ -28,7 +28,7 @@ namespace nla {
 class core;
 struct basics: common {
     basics(core *core);
-    bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n, const rational& sign);
+    bool basic_sign_lemma_on_two_monomials(const monomial& m, const monomial& n);
 
     void basic_sign_lemma_model_based_one_mon(const monomial& m, int product_sign);
     
@@ -40,47 +40,47 @@ struct basics: common {
      -ab = a(-b)
     */
     bool basic_sign_lemma(bool derived);
-    bool basic_lemma_for_mon_zero(const smon& rm, const factorization& f);
+    bool basic_lemma_for_mon_zero(const monomial& rm, const factorization& f);
 
-    void basic_lemma_for_mon_zero_model_based(const smon& rm, const factorization& f);
+    void basic_lemma_for_mon_zero_model_based(const monomial& rm, const factorization& f);
 
-    void basic_lemma_for_mon_non_zero_model_based(const smon& rm, const factorization& f);
+    void basic_lemma_for_mon_non_zero_model_based(const monomial& rm, const factorization& f);
     // x = 0 or y = 0 -> xy = 0
-    void basic_lemma_for_mon_non_zero_model_based_rm(const smon& rm, const factorization& f);
+    void basic_lemma_for_mon_non_zero_model_based_rm(const monomial& 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 smon& rm, const factorization& f);
+    bool basic_lemma_for_mon_non_zero_derived(const monomial& 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 smon& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const monomial& 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 smon& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_monomial_to_factor_derived(const monomial& 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 smon& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const monomial& 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 smon& rm, const factorization& f);
-    void basic_lemma_for_mon_neutral_model_based(const smon& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const monomial& rm, const factorization& f);
+    void basic_lemma_for_mon_neutral_model_based(const monomial& rm, const factorization& f);
     
-    bool basic_lemma_for_mon_neutral_derived(const smon& rm, const factorization& factorization);
+    bool basic_lemma_for_mon_neutral_derived(const monomial& rm, const factorization& factorization);
 
-    void basic_lemma_for_mon_model_based(const smon& rm);
+    void basic_lemma_for_mon_model_based(const monomial& rm);
 
-    bool basic_lemma_for_mon_derived(const smon& rm);
+    bool basic_lemma_for_mon_derived(const monomial& 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 smon& rm, bool derived);
+    void basic_lemma_for_mon(const monomial& 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 smon& rm, const factorization& factorization);
+    void proportion_lemma_model_based(const monomial& rm, const factorization& factorization);
     // x != 0 or y = 0 => |xy| >= |y|
-    bool proportion_lemma_derived(const smon& rm, const factorization& factorization);
+    bool proportion_lemma_derived(const monomial& 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 smon& rm, const factorization& fc, int factor_index);   
+    void generate_pl(const monomial& rm, const factorization& fc, int factor_index);   
 };
 }
diff --git a/src/util/lp/nla_common.cpp b/src/util/lp/nla_common.cpp
index dbb949808..40223ac66 100644
--- a/src/util/lp/nla_common.cpp
+++ b/src/util/lp/nla_common.cpp
@@ -28,25 +28,23 @@ template <typename T> void common::explain(const T& t) {
 }
 template void common::explain<monomial>(const monomial& t);
 template void common::explain<factor>(const factor& t);
-template void common::explain<smon>(const smon& 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 c().vvr(t); }
 template rational common::vvr<monomial>(monomial const& t) const;
-template rational common::vvr<smon>(smon const& t) const;
 template rational common::vvr<factor>(factor const& t) const;
 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<smon>(smon const& t) const;
+template lpvar common::var<monomial>(monomial 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<smon>(const smon& t) const;
+template rational common::canonize_sign<monomial>(const monomial& 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);
@@ -98,10 +96,7 @@ std::ostream& common::print_product(const T & m, std::ostream& out) const {
     return c().print_product(m, out);
 }
 template 
-std::ostream& common::print_product<monomial>(const monomial & m, std::ostream& out) const;
-
-template std::ostream& common::print_product<smon>(const smon & m, std::ostream& out) const;
-
+std::ostream& common::print_product<unsigned_vector>(const unsigned_vector & m, std::ostream& out) const;
 
 std::ostream& common::print_monomial(const monomial & m, std::ostream& out) const {
     return c().print_monomial(m, out);
diff --git a/src/util/lp/nla_common.h b/src/util/lp/nla_common.h
index e363df736..31703fb40 100644
--- a/src/util/lp/nla_common.h
+++ b/src/util/lp/nla_common.h
@@ -87,8 +87,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 smon &, std::ostream& out) const;
-    std::ostream& print_rooted_monomial_with_vars(const smon&, std::ostream& out) const;
+    std::ostream& print_rooted_monomial(const monomial &, std::ostream& out) const;
+    std::ostream& print_rooted_monomial_with_vars(const monomial&, 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 30b84cbf1..92152acac 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -83,21 +83,20 @@ svector<lpvar> core::sorted_vars(const factor& f) const {
         return r;
     }
     TRACE("nla_solver", tout << "nv";);
-    return m_emons.canonical[f.var()].rvars();
+    return m_emons[f.var()].rvars();
 }
 
 // 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.var()) : m_emons.canonical[f.var()].rsign();
+    return f.is_var()? canonize_sign_of_var(f.var()) : m_emons[f.var()].rsign();
 }
 
 rational core::canonize_sign_of_var(lpvar j) const {
     return m_evars.find(j).rsign();        
 }
     
-rational core::canonize_sign(const smon& m) const {
+rational core::canonize_sign(const monomial& m) const {
     return m.rsign();
 }
 
@@ -116,8 +115,7 @@ void core::pop(unsigned n) {
     m_emons.pop(n);
 }
 
-template <typename T>
-rational core::product_value(const T & m) const {
+rational core::product_value(const unsigned_vector & m) const {
     rational r(1);
     for (auto j : m) {
         r *= m_lar_solver.get_column_value_rational(j);
@@ -128,18 +126,14 @@ rational core::product_value(const T & m) const {
 // return true iff the monomial value is equal to the product of the values of the factors
 bool core::check_monomial(const monomial& m) const {
     SASSERT(m_lar_solver.get_column_value(m.var()).is_int());        
-    return product_value(m) == m_lar_solver.get_column_value_rational(m.var());
+    return product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var());
 }
     
 void core::explain(const monomial& m, lp::explanation& exp) const {       
-    for (lpvar j : m)
+    for (lpvar j : m.vars())
         explain(j, exp);
 }
 
-void core::explain(const smon& 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.var(), exp);
@@ -161,8 +155,6 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
     }
     return out;
 }
-template std::ostream& core::print_product<monomial>(const monomial & m, std::ostream& out) const;
-template std::ostream& core::print_product<smon>(const smon & m, std::ostream& out) const;
 
 std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
     if (f.is_var()) {
@@ -170,7 +162,7 @@ std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
         print_var(f.var(), out);
     } else {
         out << "PROD, ";
-        print_product(m_emons.canonical[f.var()].rvars(), out);
+        print_product(m_emons[f.var()].rvars(), out);
     }
     out << "\n";
     return out;
@@ -181,7 +173,7 @@ std::ostream & core::print_factor_with_vars(const factor& f, std::ostream& out)
         print_var(f.var(), out);
     } 
     else {
-        out << " RM = " << m_emons.canonical[f.var()];
+        out << " RM = " << m_emons[f.var()];
         out << "\n orig mon = " << m_emons[f.var()];
     }
     return out;
@@ -214,7 +206,7 @@ std::ostream& core::print_monomial_with_vars(lpvar v, std::ostream& out) const {
 
 template <typename T>
 std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const {
-    print_product(m, out) << "\n";
+    print_product(m.vars(), out) << "\n";
     for (unsigned k = 0; k < m.size(); k++) {
         print_var(m[k], out);
     }
@@ -223,7 +215,7 @@ 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.vars())
         print_var(j, out);
     out << ")\n";
     return out;
@@ -569,7 +561,7 @@ bool core::zero_is_an_inner_point_of_bounds(lpvar j) const {
     
 int core::rat_sign(const monomial& m) const {
     int sign = 1;
-    for (lpvar j : m) {
+    for (lpvar j : m.vars()) {
         auto v = vvr(j);
         if (v.is_neg()) {
             sign = - sign;
@@ -778,12 +770,12 @@ 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));
-    smon const* sv = m_emons.find_canonical(vars);
+    monomial 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 {
-    smon const* sv = m_emons.find_canonical(vars);
+    monomial const* sv = m_emons.find_canonical(vars);
     return sv ? &m_emons[sv->var()] : nullptr;
 }
 
@@ -806,7 +798,7 @@ void core::explain_separation_from_zero(lpvar j) {
         explain_existing_upper_bound(j);
 }
 
-int core::get_derived_sign(const smon& rm, const factorization& f) const {
+int core::get_derived_sign(const monomial& 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) {
@@ -818,7 +810,7 @@ int core::get_derived_sign(const smon& rm, const factorization& f) const {
     }
     return nla::rat_sign(sign);
 }
-void core::trace_print_monomial_and_factorization(const smon& rm, const factorization& f, std::ostream& out) const {
+void core::trace_print_monomial_and_factorization(const monomial& rm, const factorization& f, std::ostream& out) const {
     out << "rooted vars: ";
     print_product(rm.rvars(), out);
     out << "\n";
@@ -1269,7 +1261,7 @@ bool core:: mon_has_zero(const T& product) const {
     return false;
 }
 
-template bool core::mon_has_zero<monomial>(const monomial& product) const;
+template bool core::mon_has_zero<unsigned_vector>(const unsigned_vector& product) const;
 
 
 lp::lp_settings& core::settings() {
@@ -1395,7 +1387,7 @@ template <typename T>
 void core::trace_print_rms(const T& p, std::ostream& out) {
     out << "p = {\n";
     for (auto j : p) {
-        out << "j = " << j << ", rm = " << m_emons.canonical[j] << "\n";
+        out << "j = " << j << ", rm = " << m_emons[j] << "\n";
     }
     out << "}";
 }
@@ -1407,7 +1399,7 @@ 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);
-            smon const* sv = m_emons.find_canonical(vv);
+            monomial const* sv = m_emons.find_canonical(vv);
             if (!sv) {
                 out << "nf length" << vv.size() << "\n"; ;
             }
@@ -1444,7 +1436,8 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
     auto insert_j = [&](lpvar j) { 
         vars.insert(j);
         if (m_emons.is_monomial_var(j)) {
-            for (lpvar k : m_emons[j]) vars.insert(k);
+            for (lpvar k : m_emons[j].vars())
+                vars.insert(k);
         }
     };
     
@@ -1462,7 +1455,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
     return vars;
 }
 
-bool core::divide(const smon& bc, const factor& c, factor & b) const {
+bool core::divide(const monomial& bc, const factor& c, factor & b) const {
     svector<lpvar> c_vars = sorted_vars(c);
     TRACE("nla_solver_div",
           tout << "c_vars = ";
@@ -1479,7 +1472,7 @@ bool core::divide(const smon& bc, const factor& c, factor & b) const {
         b = factor(b_vars[0], factor_type::VAR);
         return true;
     }
-    smon const* sv = m_emons.find_canonical(b_vars);
+    monomial const* sv = m_emons.find_canonical(b_vars);
     if (!sv) {
         TRACE("nla_solver_div", tout << "not in rooted";);
         return false;
@@ -1529,10 +1522,10 @@ void core::print_specific_lemma(const lemma& l, std::ostream& out) const {
 }
     
 
-void core::trace_print_ol(const smon& ac,
+void core::trace_print_ol(const monomial& ac,
                           const factor& a,
                           const factor& c,
-                          const smon& bc,
+                          const monomial& bc,
                           const factor& b,
                           std::ostream& out) {
     out << "ac = " << ac << "\n";
@@ -1581,7 +1574,7 @@ std::unordered_map<unsigned, unsigned_vector> core::get_rm_by_arity() {
 
     
 
-bool core::rm_check(const smon& rm) const {
+bool core::rm_check(const monomial& rm) const {
     return check_monomial(m_emons[rm.var()]);
 }
     
@@ -1639,7 +1632,7 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
 */
 
     
-bool core::find_bfc_to_refine_on_rmonomial(const smon& rm, bfc & bf) {
+bool core::find_bfc_to_refine_on_rmonomial(const monomial& rm, bfc & bf) {
     for (auto factorization : factorization_factory_imp(rm, *this)) {
         if (factorization.size() == 2) {
             auto a = factorization[0];
@@ -1653,18 +1646,18 @@ bool core::find_bfc_to_refine_on_rmonomial(const smon& rm, bfc & bf) {
     return false;
 }
     
-bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const smon*& rm_found){
+bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*& rm_found){
     rm_found = nullptr;
     for (unsigned i: m_to_refine) {
-        const auto& rm = m_emons.canonical[i];
+        const auto& rm = m_emons[i];
         SASSERT (!check_monomial(m_emons[rm.var()]));
         if (rm.size() == 2) {
             sign = rational(1);
             const monomial & m = m_emons[rm.var()];
             j = m.var();
             rm_found = nullptr;
-            bf.m_x = factor(m[0], factor_type::VAR);
-            bf.m_y = factor(m[1], factor_type::VAR);
+            bf.m_x = factor(m.vars()[0], factor_type::VAR);
+            bf.m_y = factor(m.vars()[1], factor_type::VAR);
             return true;
         }
                 
@@ -1684,8 +1677,8 @@ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const smon*& rm
 }
 
 void core::generate_simple_sign_lemma(const rational& sign, const monomial& m) {
-    SASSERT(sign == nla::rat_sign(product_value(m)));
-    for (lpvar j : m) {
+    SASSERT(sign == nla::rat_sign(product_value(m.vars())));
+    for (lpvar j : m.vars()) {
         if (vvr(j).is_pos()) {
             mk_ineq(j, llc::LE);
         } else {
@@ -1971,7 +1964,7 @@ lbool core::test_check(
     m_lar_solver.set_status(lp::lp_status::OPTIMAL);
     return check(l);
 }
-template rational core::product_value<monomial>(const monomial & m) const;
+
 } // end of nla
 
 
diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h
index 4eaeee5dd..dadd8fa14 100644
--- a/src/util/lp/nla_core.h
+++ b/src/util/lp/nla_core.h
@@ -102,9 +102,9 @@ public:
 
     lp::impq vv(lpvar j) const { return m_lar_solver.get_column_value(j); }
     
-    lpvar var(smon const& sv) const { return sv.var(); }
+    lpvar var(monomial const& sv) const { return sv.var(); }
 
-    rational vvr(const smon& rm) const { return rm.rsign()*vvr(m_emons[rm.var()]); }
+    rational vvr_rooted(const monomial& m) const { return m.rsign()*vvr(m.var()); }
 
     rational vvr(const factor& f) const {  return f.is_var()? vvr(f.var()) : vvr(m_emons[f.var()]); }
 
@@ -122,10 +122,10 @@ public:
     
     // the value of the rooted monomias is equal to the value of the m.var() variable multiplied
     // by the canonize_sign
-    rational canonize_sign(const smon& m) const;
+    rational canonize_sign(const monomial& m) const;
     
 
-    void deregister_monomial_from_smonomials (const monomial & m, unsigned i);
+    void deregister_monomial_from_monomialomials (const monomial & m, unsigned i);
 
     void deregister_monomial_from_tables(const monomial & m, unsigned i);
 
@@ -135,14 +135,12 @@ public:
     void pop(unsigned n);
 
     rational mon_value_by_vars(unsigned i) const;
-    template <typename T>
-    rational product_value(const T & m) const;
+    rational product_value(const unsigned_vector & m) const;
     
     // return true iff the monomial value is equal to the product of the values of the factors
     bool check_monomial(const monomial& m) const;
     
     void explain(const monomial& m, lp::explanation& exp) const;
-    void explain(const smon& 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);
@@ -169,7 +167,7 @@ public:
     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 smon& rm, const factorization& f, std::ostream& out) const;
+    void trace_print_monomial_and_factorization(const monomial& 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;
@@ -177,10 +175,10 @@ public:
     void print_specific_lemma(const lemma& l, std::ostream& out) const;
     
 
-    void trace_print_ol(const smon& ac,
+    void trace_print_ol(const monomial& ac,
                         const factor& a,
                         const factor& c,
-                        const smon& bc,
+                        const monomial& bc,
                         const factor& b,
                         std::ostream& out);
 
@@ -243,7 +241,7 @@ public:
     const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
 
 
-    int get_derived_sign(const smon& rm, const factorization& f) const;
+    int get_derived_sign(const monomial& rm, const factorization& f) const;
 
 
     bool var_has_positive_lower_bound(lpvar j) const;
@@ -312,7 +310,7 @@ public:
 
     void init_to_refine();
 
-    bool divide(const smon& bc, const factor& c, factor & b) const;
+    bool divide(const monomial& bc, const factor& c, factor & b) const;
 
     void negate_factor_equality(const factor& c, const factor& d);
     
@@ -320,15 +318,15 @@ public:
 
     std::unordered_set<lpvar> collect_vars(const lemma& l) const;
 
-    bool rm_check(const smon&) const;
+    bool rm_check(const monomial&) 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 smon& rm, bfc & bf);
+    bool  find_bfc_to_refine_on_rmonomial(const monomial& rm, bfc & bf);
     
-    bool  find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const smon*& rm_found);
+    bool  find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*& 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 28785b4c9..0fa9e72e5 100644
--- a/src/util/lp/nla_monotone_lemmas.cpp
+++ b/src/util/lp/nla_monotone_lemmas.cpp
@@ -34,104 +34,6 @@ void monotone::monotonicity_lemma() {
     }
 }
 
-void monotone::print_monotone_array(const monotone_array_t& lex_sorted,
-                                    std::ostream& out) const {
-    out << "Monotone array :\n";
-    for (const auto & t : lex_sorted ){
-        out << "(";
-        print_vector(t.first, out);
-        out << "), rm[" << t.second << "]" << std::endl;
-    }
-    out <<  "}";
-}
-
-bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const monotone_array_t& lex_sorted, unsigned i, const smon& rm) {
-    const rational v = abs(vvr(rm));
-    const auto& key = lex_sorted[i].first;
-    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 smon& rmk = c().m_emons.canonical[p.second];
-        const rational vk = abs(vvr(rmk));
-        TRACE("nla_solver", tout << "rmk = " << rmk << "\n";
-              tout << "vk = " << vk << std::endl;);
-        if (vk > v) continue;
-        unsigned strict;
-        if (uniform_le(key, p.first, strict)) {
-            if (static_cast<int>(strict) != -1 && !has_zero(key)) {
-                generate_monl_strict(rm, rmk, strict);
-                return true;
-            } 
-            else if (vk < v) {
-                generate_monl(rm, rmk);
-                return true;
-            }
-        }
-            
-    }
-    return false;
-}
-
-bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const monotone_array_t& lex_sorted, unsigned i, const smon& rm) {
-    const rational v = abs(vvr(rm));
-    const auto& key = lex_sorted[i].first;
-    TRACE("nla_solver", tout << "rm = " << rm << "i = " << i << std::endl;);
-        
-    for (unsigned k = i; k-- > 0;) {
-        const auto& p = lex_sorted[k];
-        const smon& rmk = c().m_emons.canonical[p.second];
-        const rational vk = abs(vvr(rmk));
-        TRACE("nla_solver", tout << "rmk = " << rmk << "\n";
-              tout << "vk = " << vk << std::endl;);
-        if (vk < v) continue;
-        unsigned strict;
-        if (uniform_le(p.first, key, strict)) {
-            TRACE("nla_solver", tout << "strict = " << strict << std::endl;);
-            if (static_cast<int>(strict) != -1) {
-                generate_monl_strict(rmk, rm, strict);
-                return true;
-            } else {
-                SASSERT(key == p.first); 
-                if (vk < v) {
-                    generate_monl(rmk, rm);
-                    return true;
-                }
-            }
-        }
-            
-    }
-    return false;
-}
-
-bool monotone::monotonicity_lemma_on_lex_sorted_rm(const monotone_array_t& lex_sorted, unsigned i, const smon& 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 monotone_array_t& lex_sorted) {
-    for (unsigned i = 0; i < lex_sorted.size(); i++) {
-        unsigned rmi = lex_sorted[i].second;
-        const smon& 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 smon& a) const {
-    vector<std::pair<rational, lpvar>> r;
-    for (lpvar j : a.rvars()) {
-        r.push_back(std::make_pair(abs(vvr(j)), j));
-    }
-    std::sort(r.begin(), r.end(), [](const std::pair<rational, lpvar>& a,
-                                     const std::pair<rational, lpvar>& b) {
-                                      return
-                                          a.first < b.first ||
-                                                    (a.first == b.first &&
-                                                     a.second < b.second);
-                                  });
-    return r;
-} 
 
 void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
     rational av = vvr(a);
@@ -148,31 +50,9 @@ void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
     }
 }
 
-// strict version
-void monotone::generate_monl_strict(const smon& a,
-                                    const smon& b,
-                                    unsigned strict) {
-    add_empty_lemma();
-    auto akey = get_sorted_key_with_vars(a);
-    auto bkey = get_sorted_key_with_vars(b);
-    SASSERT(akey.size() == bkey.size());
-    for (unsigned i = 0; i < akey.size(); i++) {
-        if (i != strict) {
-            negate_abs_a_le_abs_b(akey[i].second, bkey[i].second, true);
-        } else {
-            mk_ineq(b[i], llc::EQ);
-            negate_abs_a_lt_abs_b(akey[i].second, bkey[i].second);
-        }
-    }
-    assert_abs_val_a_le_abs_var_b(a, b, true);
-    explain(a);
-    explain(b);
-    TRACE("nla_solver", print_lemma(tout););
-}
-
 void monotone::assert_abs_val_a_le_abs_var_b(
-    const smon& a,
-    const smon& b,
+    const monomial& a,
+    const monomial& b,
     bool strict) {
     lpvar aj = var(a);
     lpvar bj = var(b);
@@ -197,55 +77,12 @@ void monotone::negate_abs_a_lt_abs_b(lpvar a, lpvar b) {
     mk_ineq(bs, b, llc::LT); // |bj| < 0
     mk_ineq(as, a, -bs, b, llc::GE); // negate  |aj| < |bj|
 }
-
-
-// not a strict version
-void monotone::generate_monl(const smon& a,
-                             const smon& 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);
-    SASSERT(akey.size() == bkey.size());
-    for (unsigned i = 0; i < akey.size(); i++) {
-        negate_abs_a_le_abs_b(akey[i].second, bkey[i].second, false);
-    }
-    assert_abs_val_a_le_abs_var_b(a, b, false);
-    explain(a);
-    explain(b);
-    TRACE("nla_solver", print_lemma(tout););
-}
-
-std::vector<rational> monotone::get_sorted_key(const smon& rm) const {
-    std::vector<rational> r;
-    for (unsigned j : rm.rvars()) {
-        r.push_back(abs(vvr(j)));
-    }
-    std::sort(r.begin(), r.end());
-    return r;
-}
-    
-bool monotone::monotonicity_lemma_on_rms_of_same_arity(const unsigned_vector& rms) { 
-    monotone_array_t lex_sorted;
-    for (unsigned i : rms) {
-        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,
-                 const std::pair<std::vector<rational>, unsigned> &b) {
-                  return a.first < b.first;
-              });
-    TRACE("nla_solver", print_monotone_array(lex_sorted, tout););
-    return monotonicity_lemma_on_lex_sorted(lex_sorted);
-}
-
+   
 void monotone::monotonicity_lemma(monomial const& m) {
     SASSERT(!check_monomial(m));
-    if (c().mon_has_zero(m))
+    if (c().mon_has_zero(m.vars()))
         return;
-    const rational prod_val = abs(c().product_value(m));
+    const rational prod_val = abs(c().product_value(m.vars()));
     const rational m_val = abs(vvr(m));
     if (m_val < prod_val)
         monotonicity_lemma_lt(m, prod_val);
@@ -255,7 +92,7 @@ void monotone::monotonicity_lemma(monomial const& m) {
 
 void monotone::monotonicity_lemma_gt(const monomial& m, const rational& prod_val) {
     add_empty_lemma();
-    for (lpvar j : m) {
+    for (lpvar j : m.vars()) {
         c().add_abs_bound(j, llc::GT);
     }
     lpvar m_j = m.var();
@@ -271,7 +108,7 @@ void monotone::monotonicity_lemma_gt(const monomial& m, const rational& prod_val
 */
 void monotone::monotonicity_lemma_lt(const monomial& m, const rational& prod_val) {
     add_empty_lemma();
-    for (lpvar j : m) {
+    for (lpvar j : m.vars()) {
         c().add_abs_bound(j, llc::LT);
     }
     lpvar m_j = m.var();
diff --git a/src/util/lp/nla_monotone_lemmas.h b/src/util/lp/nla_monotone_lemmas.h
index c480460c6..47bdc3be6 100644
--- a/src/util/lp/nla_monotone_lemmas.h
+++ b/src/util/lp/nla_monotone_lemmas.h
@@ -25,22 +25,13 @@ public:
     monotone(core *core);
     void monotonicity_lemma();
 private:
-    typedef vector<std::pair<std::vector<rational>, unsigned>> monotone_array_t;
-    void print_monotone_array(const monotone_array_t& lex_sorted, std::ostream& out) const;
-    bool monotonicity_lemma_on_lex_sorted_rm_upper(const monotone_array_t& lex_sorted, unsigned i, const smon& rm);
-    bool monotonicity_lemma_on_lex_sorted_rm_lower(const monotone_array_t& lex_sorted, unsigned i, const smon& rm);
-    bool monotonicity_lemma_on_lex_sorted_rm(const monotone_array_t& lex_sorted, unsigned i, const smon& rm);
-    bool monotonicity_lemma_on_lex_sorted(const monotone_array_t& lex_sorted);
-    bool  monotonicity_lemma_on_rms_of_same_arity(const unsigned_vector& rms);
     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 smon& a, const smon& b,  unsigned strict);
-    void generate_monl(const smon& a, const smon& b);
-    std::vector<rational> get_sorted_key(const smon& rm) const;
-    vector<std::pair<rational, lpvar>> get_sorted_key_with_vars(const smon& a) const;
+    std::vector<rational> get_sorted_key(const monomial& rm) const;
+    vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monomial& 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 smon& a, const smon& b, bool strict);
+    void assert_abs_val_a_le_abs_var_b(const monomial& a, const monomial& b, bool strict);
 };
 }
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index f6b828990..fb4725dc8 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -30,22 +30,22 @@ void order::order_lemma() {
     unsigned start = random();
     unsigned sz = rm_ref.size();
     for (unsigned i = 0; i < sz && !done(); ++i) {        
-        const smon& rm = c().m_emons.canonical[rm_ref[(i + start) % sz]];
+        const monomial& rm = c().m_emons[rm_ref[(i + start) % sz]];
         order_lemma_on_rmonomial(rm);
     }
 }
 
-void order::order_lemma_on_rmonomial(const smon& rm) {
+void order::order_lemma_on_rmonomial(const monomial& m) {
     TRACE("nla_solver_details",
-          tout << "rm = " << rm << ", orig = " << pp_mon(c(), c().m_emons[rm]););
+          tout << "m = " << pp_mon(c(), m););
 
-    for (auto ac : factorization_factory_imp(rm, c())) {
+    for (auto ac : factorization_factory_imp(m, c())) {
         if (ac.size() != 2)
             continue;
         if (ac.is_mon())
             order_lemma_on_binomial(*ac.mon());
         else
-            order_lemma_on_factorization(rm, ac);
+            order_lemma_on_factorization(m, ac);
         if (done())
             break;
     }
@@ -54,7 +54,7 @@ void order::order_lemma_on_rmonomial(const smon& rm) {
 void order::order_lemma_on_binomial(const monomial& ac) {
     TRACE("nla_solver", tout << pp_mon(c(), ac););
     SASSERT(!check_monomial(ac) && ac.size() == 2);
-    const rational mult_val = vvr(ac[0]) * vvr(ac[1]);
+    const rational mult_val = vvr(ac.vars()[0]) * vvr(ac.vars()[1]);
     const rational acv = vvr(ac);
     bool gt = acv > mult_val;
     for (unsigned k = 0; k < 2; k++) {
@@ -64,8 +64,8 @@ void order::order_lemma_on_binomial(const monomial& ac) {
 }
 
 void order::order_lemma_on_binomial_k(const monomial& m, bool k, bool gt) {
-    SASSERT(gt == (vvr(m) > vvr(m[0]) * vvr(m[1])));
-    order_lemma_on_binomial_sign(m, m[k], m[!k], gt ? 1: -1);
+    SASSERT(gt == (vvr(m) > vvr(m.vars()[0]) * vvr(m.vars()[1])));
+    order_lemma_on_binomial_sign(m, m.vars()[k], m.vars()[!k], gt ? 1: -1);
 }
 
 /**
@@ -78,7 +78,7 @@ void order::order_lemma_on_binomial_k(const monomial& m, bool k, bool gt) {
   
 */
 void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, int sign) {
-    SASSERT(!_().mon_has_zero(xy));
+    SASSERT(!_().mon_has_zero(xy.vars()));
     int sy = rat_sign(vvr(y));
     add_empty_lemma();
     mk_ineq(y,                     sy == 1      ? llc::LE : llc::GE); // negate sy
@@ -89,7 +89,7 @@ void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, i
 
 void order::order_lemma_on_factor_binomial_explore(const monomial& m1, bool k) {
     SASSERT(m1.size() == 2);
-    lpvar c = m1[k];
+    lpvar c = m1.vars()[k];
     for (monomial const& m2 : _().m_emons.get_factors_of(c)) {
         order_lemma_on_factor_binomial_rm(m1, k, m2);
         if (done()) {
@@ -99,20 +99,19 @@ void order::order_lemma_on_factor_binomial_explore(const monomial& m1, bool k) {
 }
 
 void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd) {
-    smon const& rm_bd = _().m_emons.canonical[bd];
-    factor d(_().m_evars.find(ac[k]).var(), factor_type::VAR);
+    factor d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR);
     factor b;
-    if (c().divide(rm_bd, d, b)) {
-        order_lemma_on_binomial_ac_bd(ac, k, rm_bd, b, d.var());
+    if (c().divide(bd, d, b)) {
+        order_lemma_on_binomial_ac_bd(ac, k, bd, b, d.var());
     }
 }
 
-void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const smon& bd, const factor& b, lpvar d) {
+void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d) {
     TRACE("nla_solver",  
           tout << "ac=" << pp_mon(c(), ac) << "\nrm= " << bd << ", b= " << pp_fac(c(), b) << ", d= " << pp_var(c(), d) << "\n";);
     bool p = !k;
-    lpvar a = ac[p];
-    lpvar c = ac[k];
+    lpvar a = ac.vars()[p];
+    lpvar c = ac.vars()[k];
     SASSERT(_().m_evars.find(c).var() == d);
     rational acv = vvr(ac);
     rational av = vvr(a);
@@ -137,7 +136,7 @@ void order::generate_mon_ol(const monomial& ac,
                            lpvar a,
                            const rational& c_sign,
                            lpvar c,
-                           const smon& bd,
+                           const monomial& bd,
                            const factor& b,
                            const rational& d_sign,
                            lpvar d,
@@ -159,10 +158,10 @@ void order::generate_mon_ol(const monomial& ac,
 // a >< b && c < 0 => ac <> bc
 // ac[k] plays the role of c   
 
-bool order::order_lemma_on_ac_and_bc(const smon& rm_ac,
+bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac,
                                      const factorization& ac_f,
                                      bool k,
-                                     const smon& rm_bd) {
+                                     const monomial& rm_bd) {
     TRACE("nla_solver", 
           tout << "rm_ac = " << rm_ac << "\n";
           tout << "rm_bd = " << rm_bd << "\n";
@@ -176,10 +175,8 @@ bool order::order_lemma_on_ac_and_bc(const smon& rm_ac,
 
 // TBD: document what lemma is created here.
 
-void order::order_lemma_on_factorization(const smon& rm, const factorization& ab) {
-    const monomial& m = _().m_emons[rm];
-    TRACE("nla_solver", tout << "orig_sign = " << _().m_emons.orig_sign(rm) << "\n";);
-    rational sign = _().m_emons.orig_sign(rm);
+void order::order_lemma_on_factorization(const monomial& m, const factorization& ab) {
+    rational sign = m.rsign();
     for (factor f: ab)
         sign *= _().canonize_sign(f);
     const rational fv = vvr(ab[0]) * vvr(ab[1]);
@@ -194,26 +191,25 @@ void order::order_lemma_on_factorization(const smon& rm, const factorization& ab
     for (unsigned j = 0, k = 1; j < 2; j++, k--) {
         order_lemma_on_ab(m, sign, var(ab[k]), var(ab[j]), gt);
         explain(ab); explain(m);
-        explain(rm);
         TRACE("nla_solver", _().print_lemma(tout););
-        order_lemma_on_ac_explore(rm, ab, j == 1);
+        order_lemma_on_ac_explore(m, ab, j == 1);
     }
 }
 
-bool order::order_lemma_on_ac_explore(const smon& rm, const factorization& ac, bool k) {
+bool order::order_lemma_on_ac_explore(const monomial& rm, const factorization& ac, bool 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 (monomial const& bc : _().m_emons.get_use_list(c.var())) {
-            if (order_lemma_on_ac_and_bc(rm ,ac, k, _().m_emons.canonical[bc])) {
+            if (order_lemma_on_ac_and_bc(rm ,ac, k, bc)) {
                 return true;
             }
         }
     } 
     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])) {
+            if (order_lemma_on_ac_and_bc(rm , ac, k, bc)) {
                 return true;
             }
         }
@@ -223,11 +219,11 @@ bool order::order_lemma_on_ac_explore(const smon& rm, const factorization& ac, b
 
 // |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 smon& ac,                     
+void order::generate_ol(const monomial& ac,                     
                        const factor& a,
                        int c_sign,
                        const factor& c,
-                       const smon& bc,
+                       const monomial& bc,
                        const factor& b,
                        llc ab_cmp) {
     add_empty_lemma();
@@ -251,10 +247,10 @@ void order::negate_var_factor_relation(const rational& a_sign, lpvar a, const ra
 }
 
 
-bool order::order_lemma_on_ac_and_bc_and_factors(const smon& ac,
+bool order::order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
                                                  const factor& a,
                                                  const factor& c,
-                                                 const smon& bc,
+                                                 const monomial& bc,
                                                  const factor& b) {
     auto cv = vvr(c); 
     int c_sign = nla::rat_sign(cv);
diff --git a/src/util/lp/nla_order_lemmas.h b/src/util/lp/nla_order_lemmas.h
index b32478230..9ccb66b11 100644
--- a/src/util/lp/nla_order_lemmas.h
+++ b/src/util/lp/nla_order_lemmas.h
@@ -31,23 +31,23 @@ public:
     
 private:
 
-    bool order_lemma_on_ac_and_bc_and_factors(const smon& ac,
+    bool order_lemma_on_ac_and_bc_and_factors(const monomial& ac,
                                               const factor& a,
                                               const factor& c,
-                                              const smon& bc,
+                                              const monomial& 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 smon& rm_ac,
+    bool order_lemma_on_ac_and_bc(const monomial& rm_ac,
                                   const factorization& ac_f,
                                   bool k,
-                                  const smon& rm_bd);
+                                  const monomial& rm_bd);
     
-    bool order_lemma_on_ac_explore(const smon& rm, const factorization& ac, bool k);
+    bool order_lemma_on_ac_explore(const monomial& rm, const factorization& ac, bool k);
 
-    void order_lemma_on_factorization(const smon& rm, const factorization& ab);
+    void order_lemma_on_factorization(const monomial& rm, const factorization& ab);
     
     /**
        \brief Add lemma: 
@@ -65,18 +65,18 @@ private:
     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, bool k);
     void order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd);
-    void order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const smon& bd, const factor& b, lpvar d);
+    void order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d);
     void order_lemma_on_binomial_k(const monomial& m, bool 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 smon& rm);
+    void order_lemma_on_rmonomial(const monomial& rm);
     // |c_sign| = 1, and c*c_sign > 0
     // ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
-    void generate_ol(const smon& ac,                     
+    void generate_ol(const monomial& ac,                     
                      const factor& a,
                      int c_sign,
                      const factor& c,
-                     const smon& bc,
+                     const monomial& bc,
                      const factor& b,
                      llc ab_cmp);
 
@@ -84,7 +84,7 @@ private:
                          lpvar a,
                          const rational& c_sign,
                          lpvar c,
-                         const smon& bd,
+                         const monomial& bd,
                          const factor& b,
                          const rational& d_sign,
                          lpvar d,
diff --git a/src/util/lp/nla_tangent_lemmas.cpp b/src/util/lp/nla_tangent_lemmas.cpp
index 79534228d..5d44eaa49 100644
--- a/src/util/lp/nla_tangent_lemmas.cpp
+++ b/src/util/lp/nla_tangent_lemmas.cpp
@@ -30,13 +30,12 @@ std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std
     return out << "(" << a <<  ", " << b << ")";
 }
 
-void tangents::generate_simple_tangent_lemma(const smon* rm) {
-    if (rm->size() != 2)
+void tangents::generate_simple_tangent_lemma(const monomial& m) {
+    if (m.size() != 2)
         return;
-    TRACE("nla_solver", tout << "rm:" << *rm << std::endl;);
-    m_core->add_empty_lemma();
-    const monomial & m = c().m_emons[rm->var()];
-    const rational v = c().product_value(m);
+    TRACE("nla_solver", tout << "m:" << pp_mon(c(), m) << std::endl;);
+    c().add_empty_lemma();
+    const rational v = c().product_value(m.vars());
     const rational mv = vvr(m);
     SASSERT(mv != v);
     SASSERT(!mv.is_zero() && !v.is_zero());
@@ -47,15 +46,15 @@ void tangents::generate_simple_tangent_lemma(const smon* rm) {
     }
     bool gt = abs(mv) > abs(v);
     if (gt) {
-        for (lpvar j : m) {
+        for (lpvar j : m.vars()) {
             const rational jv = vvr(j);
             rational js = rational(nla::rat_sign(jv));
             c().mk_ineq(js, j, llc::LT);
             c().mk_ineq(js, j, llc::GT, jv);
         }
-        c().mk_ineq(sign, rm->var(), llc::LE, std::max(v, rational(-1)));
+        c().mk_ineq(sign, m.var(), llc::LE, std::max(v, rational(-1)));
     } else {
-        for (lpvar j : m) {
+        for (lpvar j : m.vars()) {
             const rational jv = vvr(j);
             rational js = rational(nla::rat_sign(jv));
             c().mk_ineq(js, j, llc::LT, std::max(jv, rational(0)));
@@ -70,18 +69,18 @@ void tangents::tangent_lemma() {
     bfc bf;
     lpvar j;
     rational sign;
-    const smon* rm = nullptr;
+    const monomial* rm = nullptr;
         
     if (c().find_bfc_to_refine(bf, j, sign, rm)) {
         tangent_lemma_bf(bf, j, sign, rm);
     } else {
         TRACE("nla_solver", tout << "cannot find a bfc to refine\n"; );
         if (rm != nullptr)
-            generate_simple_tangent_lemma(rm);
+            generate_simple_tangent_lemma(*rm);
     }
 }
 
-void tangents::generate_explanations_of_tang_lemma(const smon& rm, const bfc& bf, lp::explanation& exp) {
+void tangents::generate_explanations_of_tang_lemma(const monomial& 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);
@@ -109,7 +108,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 smon* rm){
+void tangents::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const monomial* 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 62e6d7979..e5ac673c6 100644
--- a/src/util/lp/nla_tangent_lemmas.h
+++ b/src/util/lp/nla_tangent_lemmas.h
@@ -54,11 +54,11 @@ public:
     void tangent_lemma();
 private:
 
-    void generate_simple_tangent_lemma(const smon* rm);    
+    void generate_simple_tangent_lemma(const monomial&);    
 
-    void generate_explanations_of_tang_lemma(const smon& rm, const bfc& bf, lp::explanation& exp);
+    void generate_explanations_of_tang_lemma(const monomial& rm, const bfc& bf, lp::explanation& exp);
     
-    void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const smon* rm);
+    void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const monomial* 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);
diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp
index 544a075bf..d95680671 100644
--- a/src/util/lp/nra_solver.cpp
+++ b/src/util/lp/nra_solver.cpp
@@ -13,7 +13,8 @@
 
 namespace nra {
 
-typedef nla::monomial mon_eq;
+typedef nla::mon_eq mon_eq;
+
 typedef nla::variable_map_type variable_map_type;
     struct solver::imp {
         lp::lar_solver&      s;
@@ -136,7 +137,7 @@ typedef nla::variable_map_type variable_map_type;
         void add_monomial_eq(mon_eq const& m) {
             polynomial::manager& pm = m_nlsat->pm();
             svector<polynomial::var> vars;
-            for (auto v : m) {
+            for (auto v : m.vars()) {
                 vars.push_back(lp2nl(v));
             }
             polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm);
@@ -227,7 +228,7 @@ typedef nla::variable_map_type variable_map_type;
         std::ostream& display(std::ostream& out) const {
             for (auto m : m_monomials) {
                 out << "v" << m.var() << " = ";
-                for (auto v : m) {
+                for (auto v : m.vars()) {
                     out << "v" << v << " ";
                 }
                 out << "\n";