diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp
index c5621ce19..e2bcc0b84 100644
--- a/src/util/lp/emonomials.cpp
+++ b/src/util/lp/emonomials.cpp
@@ -132,7 +132,8 @@ namespace nla {
         return m_use_lists[v].m_head;
     }
 
-    signed_vars const* emonomials::find_canonical(svector<lpvar> const& vars) const { 
+    smon 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();
         for (unsigned i = 0; i < m_var2index.size(); ++i) {
@@ -143,10 +144,10 @@ namespace nla {
         }
         unsigned idx = m_monomials.size();
         m_monomials.push_back(monomial(v, vars.size(), vars.c_ptr()));
-        m_canonized.push_back(signed_vars_ts(v, idx));
+        m_canonized.push_back(smon_ts(v, idx));
         m_var2index.setx(v, idx, UINT_MAX);
         do_canonize(m_monomials[idx]);
-        signed_vars const* result = nullptr;
+        smon const* result = nullptr;
         lpvar w; 
         if (m_cg_table.find(v, w)) {
             SASSERT(w != v);
@@ -179,7 +180,7 @@ namespace nla {
     }
 
     void emonomials::remove_cg(unsigned idx, monomial const& m) {
-        signed_vars_ts& sv = m_canonized[idx];
+        smon_ts& sv = m_canonized[idx];
         unsigned next = sv.m_next;
         unsigned prev = sv.m_prev;
         
@@ -203,7 +204,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 (signed_vars) are considered
+       variable equivalences. The canonized monomials (smon) are considered
        in the same equivalence class if they have the same set of representative
        variables. Their signs may differ.       
     */
@@ -258,13 +259,13 @@ namespace nla {
        \brief insert a new monomial.
 
        Assume that the variables are canonical, that is, not equal in current
-       context so another variable. The monomial is inserted into a congruence
+       context to another variable. The monomial is inserted into a congruence
        class of equal up-to var_eqs monomials.
      */
     void emonomials::add(lpvar v, unsigned sz, lpvar const* vs) {
         unsigned idx = m_monomials.size();
         m_monomials.push_back(monomial(v, sz, vs));
-        m_canonized.push_back(signed_vars_ts(v, idx));
+        m_canonized.push_back(smon_ts(v, idx));
         lpvar last_var = UINT_MAX;
         for (unsigned i = 0; i < sz; ++i) {
             lpvar w = vs[i];
@@ -282,7 +283,7 @@ namespace nla {
 
     void emonomials::do_canonize(monomial const& mon) const {
         unsigned index = m_var2index[mon.var()];
-        signed_vars& svs = m_canonized[index];
+        smon& svs = m_canonized[index];
         svs.reset();
         for (lpvar v : mon) {
             svs.push_var(m_ve.find(v));
@@ -292,8 +293,8 @@ namespace nla {
 
     bool emonomials::canonize_divides(monomial const& m1, monomial const& m2) const {
         if (m1.size() > m2.size()) return false;
-        signed_vars const& s1 = canonize(m1);
-        signed_vars const& s2 = canonize(m2);
+        smon const& s1 = canonize(m1);
+        smon const& s2 = canonize(m2);
         unsigned sz1 = s1.size(), sz2 = s2.size();
         unsigned i = 0, j = 0;
         while (true) {
diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h
index e34e72c96..5ad7ea70a 100644
--- a/src/util/lp/emonomials.h
+++ b/src/util/lp/emonomials.h
@@ -31,12 +31,12 @@ namespace nla {
        \brief class used to summarize the coefficients to a monomial after
        canonization with respect to current equalities.
     */
-    class signed_vars {
+    class smon {
         lpvar           m_var; // variable representing original monomial
         svector<lpvar>  m_vars;
         bool            m_sign;
     public:
-        signed_vars(lpvar v) : m_var(v), m_sign(false) {}
+        smon(lpvar v) : m_var(v), m_sign(false) {}
         lpvar var() const { return m_var; }
         svector<lpvar> const& vars() const { return m_vars; }
         svector<lp::var_index>::const_iterator begin() const { return vars().begin(); }
@@ -58,7 +58,7 @@ namespace nla {
         }
     };
 
-    inline std::ostream& operator<<(std::ostream& out, signed_vars const& m) { return m.display(out); }
+    inline std::ostream& operator<<(std::ostream& out, smon const& m) { return m.display(out); }
 
 
     class emonomials : public var_eqs_merge_handler {
@@ -86,9 +86,9 @@ namespace nla {
         /**
            \brief private fields used by emonomials for maintaining state of canonized monomials.
         */
-        class signed_vars_ts : public signed_vars {
+        class smon_ts : public smon {
         public:
-            signed_vars_ts(lpvar v, unsigned idx): signed_vars(v), m_next(idx), m_prev(idx), m_visited(0) {}
+            smon_ts(lpvar v, unsigned idx): smon(v), m_next(idx), m_prev(idx), m_visited(0) {}
             unsigned m_next;                    // next congruent node.
             unsigned m_prev;                    // previous congruent node
             mutable unsigned m_visited;
@@ -120,7 +120,7 @@ namespace nla {
         unsigned_vector                 m_lim;           // backtracking point
         mutable unsigned                m_visited;       // timestamp of visited monomials during pf_iterator
         region                          m_region;        // region for allocating linked lists
-        mutable vector<signed_vars_ts>  m_canonized;     // canonized versions of signed variables
+        mutable vector<smon_ts>  m_canonized;     // canonized versions of signed variables
         mutable svector<head_tail>      m_use_lists;     // use list of monomials where variables occur.
         hash_canonical                  m_cg_hash;
         eq_canonical                    m_cg_eq;
@@ -189,14 +189,14 @@ namespace nla {
         /**
            \brief retrieve canonized monomial corresponding to variable v from definition v := vs
         */
-        signed_vars const& var2canonical(lpvar v) const { return canonize(var2monomial(v)); }
+        smon const& var2canonical(lpvar v) const { return canonize(var2monomial(v)); }
         
         class canonical {
             emonomials& m;
         public:
             canonical(emonomials& m): m(m) {}
-            signed_vars const& operator[](lpvar v) const { return m.var2canonical(v); }
-            signed_vars const& operator[](monomial const& mon) const { return m.var2canonical(mon.var()); }
+            smon const& operator[](lpvar v) const { return m.var2canonical(v); }
+            smon const& operator[](monomial const& mon) const { return m.var2canonical(mon.var()); }
         };
 
         canonical canonical;
@@ -205,13 +205,13 @@ namespace nla {
            \brief obtain a canonized signed monomial
            corresponding to current equivalence class.
         */
-        signed_vars const& canonize(monomial const& m) const { return m_canonized[m_var2index[m.var()]]; }
+        smon const& canonize(monomial const& m) const { return m_canonized[m_var2index[m.var()]]; }
 
         /**
            \brief obtain the representative canonized monomial up to sign.
         */
-        //signed_vars const& rep(signed_vars const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
-        signed_vars const& rep(signed_vars const& sv) const {
+        //smon const& rep(smon const& sv) const { return m_canonized[m_var2index[m_cg_table[sv.var()]]]; }
+        smon const& rep(smon const& sv) const {
             unsigned j = -1;
             m_cg_table.find(sv.var(), j);
             return m_canonized[m_var2index[j]];
@@ -220,7 +220,7 @@ namespace nla {
         /**
            \brief the original sign is defined as a sign of the equivalence class representative.
         */
-        rational orig_sign(signed_vars const& sv) const { return rep(sv).rsign(); }           
+        rational orig_sign(smon const& sv) const { return rep(sv).rsign(); }           
 
         /**
            \brief determine if m1 divides m2 over the canonization obtained from merged variables.
@@ -301,7 +301,7 @@ namespace nla {
         factors_of get_factors_of(monomial const& m) const { inc_visited(); return factors_of(*this, m); }
         factors_of get_factors_of(lpvar v) const { inc_visited(); return factors_of(*this, v); }
        
-        signed_vars const* find_canonical(svector<lpvar> const& vars) const;
+        smon const* find_canonical(svector<lpvar> const& vars) const;
 
         /**
            \brief iterator over sign equivalent monomials.
@@ -350,7 +350,7 @@ namespace nla {
 
         sign_equiv_monomials enum_sign_equiv_monomials(monomial const& m) { return sign_equiv_monomials(*this, m); }
         sign_equiv_monomials enum_sign_equiv_monomials(lpvar v) { return enum_sign_equiv_monomials((*this)[v]); }
-        sign_equiv_monomials enum_sign_equiv_monomials(signed_vars const& sv) { return enum_sign_equiv_monomials(sv.var()); }
+        sign_equiv_monomials enum_sign_equiv_monomials(smon const& sv) { return enum_sign_equiv_monomials(sv.var()); }
 
         /**
            \brief display state of emonomials
diff --git a/src/util/lp/factorization_factory_imp.cpp b/src/util/lp/factorization_factory_imp.cpp
index d8ef706df..9d9baac18 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 signed_vars& rm, const core& s) :
+factorization_factory_imp::factorization_factory_imp(const smon& rm, const core& s) :
     factorization_factory(rm.vars(), &s.m_emons[rm.var()]),
     m_core(s), m_mon(s.m_emons[rm.var()]), m_rm(rm) { }
         
diff --git a/src/util/lp/factorization_factory_imp.h b/src/util/lp/factorization_factory_imp.h
index 81b6b0037..5f674026d 100644
--- a/src/util/lp/factorization_factory_imp.h
+++ b/src/util/lp/factorization_factory_imp.h
@@ -21,14 +21,14 @@
 #include "util/lp/factorization.h"
 namespace nla {
     class  core;
-    class signed_vars;
+    class smon;
 
     struct factorization_factory_imp: factorization_factory {
         const core&  m_core;
         const monomial & m_mon;
-        const signed_vars& m_rm;
+        const smon& m_rm;
         
-        factorization_factory_imp(const signed_vars& rm, const core& s);
+        factorization_factory_imp(const smon& 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/lar_solver.h b/src/util/lp/lar_solver.h
index 75ca8d5fe..35f138f80 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -246,6 +246,7 @@ public:
 
     void clear();
     lar_solver();
+
     void set_track_pivoted_rows(bool v);
 
     bool get_track_pivoted_rows() const;
diff --git a/src/util/lp/monomial.h b/src/util/lp/monomial.h
index 10f2e99e9..321c24000 100644
--- a/src/util/lp/monomial.h
+++ b/src/util/lp/monomial.h
@@ -1,7 +1,7 @@
 /*
   Copyright (c) 2017 Microsoft Corporation
   Author: Nikolaj Bjorner
-          Lev Nachmanson
+  Lev Nachmanson
       
 */
 #pragma once
@@ -10,33 +10,33 @@
 #include "util/lp/lar_solver.h"
 
 namespace nla {
-    /*
-     *  represents definition m_v = v1*v2*...*vn, 
-     *  where m_vs = [v1, v2, .., vn]
-     */
-    class monomial {
-        // 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):
-           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):
-           m_v(v), m_vs(vs) {
-            std::sort(m_vs.begin(), m_vs.end());
-        }
-        monomial() {}
+/*
+ *  represents definition m_v = v1*v2*...*vn, 
+ *  where m_vs = [v1, v2, .., vn]
+ */
+class monomial {
+    // 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):
+        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):
+        m_v(v), m_vs(vs) {
+        std::sort(m_vs.begin(), m_vs.end());
+    }
+    monomial() {}
         
-        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; }
-        bool empty() const { return m_vs.empty(); }
+    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; }
+    bool empty() const { return m_vs.empty(); }
 
         std::ostream& display(std::ostream& out) const {
             out << "v" << var() << " := ";
@@ -48,16 +48,17 @@ namespace nla {
     };
 
     inline std::ostream& operator<<(std::ostream& out, monomial const& m) {
+        SASSERT(false);
         return m.display(out);
     }
 
     typedef std::unordered_map<lp::var_index, rational> variable_map_type;
     
-    bool check_assignment(monomial const& m, variable_map_type & vars);
+bool check_assignment(monomial const& m, variable_map_type & vars);
     
-    bool check_assignments(const vector<monomial> & monomimials,
-                           const lp::lar_solver& s,
-                           variable_map_type & vars);
+bool check_assignments(const vector<monomial> & monomimials,
+                       const lp::lar_solver& s,
+                       variable_map_type & vars);
 
 
 
diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp
index 1084d1761..e5e7fcc76 100644
--- a/src/util/lp/nla_basics_lemmas.cpp
+++ b/src/util/lp/nla_basics_lemmas.cpp
@@ -122,11 +122,11 @@ bool basics::basic_sign_lemma_on_mon(lpvar v, std::unordered_set<unsigned> & exp
     }
 
     const monomial& m_v = c().m_emons[v];
-    signed_vars const& sv_v = c().m_emons.canonical[v];
-    TRACE("nla_solver_details", tout << "mon = " << m_v;);
+    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)) {
-        signed_vars const& sv_w = c().m_emons.canonical[m_w];
+        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()) 
             return true;
     }
@@ -222,7 +222,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 signed_vars& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_zero(const smon& rm, const factorization& f) {
     NOT_IMPLEMENTED_YET();
     return true;
 #if 0
@@ -251,7 +251,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 signed_vars& r = c().m_emons.canonical[v];
+        const smon& r = c().m_emons.canonical[v];
         SASSERT (!c().check_monomial(c().m_emons[v]));
         basic_lemma_for_mon(r, derived);
     } 
@@ -261,13 +261,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 signed_vars& rm, bool derived) {
+void basics::basic_lemma_for_mon(const smon& 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 signed_vars& rm) {
+bool basics::basic_lemma_for_mon_derived(const smon& rm) {
     if (c().var_is_fixed_to_zero(var(rm))) {
         for (auto factorization : factorization_factory_imp(rm, c())) {
             if (factorization.is_empty())
@@ -293,7 +293,7 @@ bool basics::basic_lemma_for_mon_derived(const signed_vars& rm) {
     return false;
 }
 // x = 0 or y = 0 -> xy = 0
-bool basics::basic_lemma_for_mon_non_zero_derived(const signed_vars& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_non_zero_derived(const smon& 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 +317,7 @@ bool basics::basic_lemma_for_mon_non_zero_derived(const signed_vars& rm, const f
 }
 // 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 signed_vars& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const smon& 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();
@@ -377,7 +377,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_derived(const signed
 }
 // use the fact
 // 1 * 1 ... * 1 * x * 1 ... * 1 = x
-bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const signed_vars& rm, const factorization& f) {
+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;
@@ -424,7 +424,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_derived(const
     return true;
 }
 
-bool basics::basic_lemma_for_mon_neutral_derived(const signed_vars& rm, const factorization& factorization) {
+bool basics::basic_lemma_for_mon_neutral_derived(const smon& 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);
@@ -432,7 +432,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const signed_vars& rm, const fa
 }
 
 // x != 0 or y = 0 => |xy| >= |y|
-void basics::proportion_lemma_model_based(const signed_vars& rm, const factorization& factorization) {
+void basics::proportion_lemma_model_based(const smon& rm, const factorization& factorization) {
     rational rmv = abs(vvr(rm));
     if (rmv.is_zero()) {
         SASSERT(c().has_zero_factor(factorization));
@@ -448,7 +448,7 @@ void basics::proportion_lemma_model_based(const signed_vars& rm, const factoriza
     }
 }
 // x != 0 or y = 0 => |xy| >= |y|
-bool basics::proportion_lemma_derived(const signed_vars& rm, const factorization& factorization) {
+bool basics::proportion_lemma_derived(const smon& rm, const factorization& factorization) {
     return false;
     rational rmv = abs(vvr(rm));
     if (rmv.is_zero()) {
@@ -489,7 +489,7 @@ 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 signed_vars& rm, const factorization& fc, int factor_index) {
+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);
@@ -523,7 +523,7 @@ void basics::generate_pl(const signed_vars& rm, const factorization& fc, int fac
     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 signed_vars& rm, const factorization& f) {        
+void basics::basic_lemma_for_mon_zero_model_based(const smon& 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 +544,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const signed_vars& rm, const f
     TRACE("nla_solver", c().print_lemma(tout););
 }
 
-void basics::basic_lemma_for_mon_model_based(const signed_vars& rm) {
+void basics::basic_lemma_for_mon_model_based(const smon& rm) {
     TRACE("nla_solver_bl", tout << "rm = " << rm;);
     if (vvr(rm).is_zero()) {
         for (auto factorization : factorization_factory_imp(rm, c())) {
@@ -664,7 +664,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 signed_vars& rm, const factorization& f) {
+bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const smon& 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 +722,7 @@ bool basics::basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const si
     return true;
 }
 
-void basics::basic_lemma_for_mon_neutral_model_based(const signed_vars& rm, const factorization& f) {
+void basics::basic_lemma_for_mon_neutral_model_based(const smon& 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,7 +734,7 @@ void basics::basic_lemma_for_mon_neutral_model_based(const signed_vars& rm, cons
 }
 // use the fact
 // 1 * 1 ... * 1 * x * 1 ... * 1 = x
-bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const signed_vars& rm, const factorization& f) {
+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);
     TRACE("nla_solver_bl", tout << "f = "; c().print_factorization(f, tout); tout << ", sign = " << sign << '\n'; );
     lpvar not_one = -1;
@@ -815,7 +815,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 signed_vars& rm, const factorization& f) {
+void basics::basic_lemma_for_mon_non_zero_model_based(const smon& 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 62f1ff9d9..494e5b8ca 100644
--- a/src/util/lp/nla_basics_lemmas.h
+++ b/src/util/lp/nla_basics_lemmas.h
@@ -40,47 +40,47 @@ struct basics: common {
      -ab = a(-b)
     */
     bool basic_sign_lemma(bool derived);
-    bool basic_lemma_for_mon_zero(const signed_vars& rm, const factorization& f);
+    bool basic_lemma_for_mon_zero(const smon& rm, const factorization& f);
 
-    void basic_lemma_for_mon_zero_model_based(const signed_vars& rm, const factorization& f);
+    void basic_lemma_for_mon_zero_model_based(const smon& rm, const factorization& f);
 
-    void basic_lemma_for_mon_non_zero_model_based(const signed_vars& rm, const factorization& f);
+    void basic_lemma_for_mon_non_zero_model_based(const smon& rm, const factorization& f);
     // x = 0 or y = 0 -> xy = 0
-    void basic_lemma_for_mon_non_zero_model_based_rm(const signed_vars& rm, const factorization& f);
+    void basic_lemma_for_mon_non_zero_model_based_rm(const smon& 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 signed_vars& rm, const factorization& f);
+    bool basic_lemma_for_mon_non_zero_derived(const smon& 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 signed_vars& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_monomial_to_factor_model_based(const smon& 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 signed_vars& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_monomial_to_factor_derived(const smon& 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 signed_vars& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const smon& 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 signed_vars& rm, const factorization& f);
-    void basic_lemma_for_mon_neutral_model_based(const signed_vars& rm, const factorization& f);
+    bool basic_lemma_for_mon_neutral_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_derived(const signed_vars& rm, const factorization& factorization);
+    bool basic_lemma_for_mon_neutral_derived(const smon& rm, const factorization& factorization);
 
-    void basic_lemma_for_mon_model_based(const signed_vars& rm);
+    void basic_lemma_for_mon_model_based(const smon& rm);
 
-    bool basic_lemma_for_mon_derived(const signed_vars& rm);
+    bool basic_lemma_for_mon_derived(const smon& 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 signed_vars& rm, bool derived);
+    void basic_lemma_for_mon(const smon& 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 signed_vars& rm, const factorization& factorization);
+    void proportion_lemma_model_based(const smon& rm, const factorization& factorization);
     // x != 0 or y = 0 => |xy| >= |y|
-    bool proportion_lemma_derived(const signed_vars& rm, const factorization& factorization);
+    bool proportion_lemma_derived(const smon& 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 signed_vars& rm, const factorization& fc, int factor_index);   
+    void generate_pl(const smon& rm, const factorization& fc, int factor_index);   
 };
 }
diff --git a/src/util/lp/nla_common.cpp b/src/util/lp/nla_common.cpp
index 8de119271..be36f51a7 100644
--- a/src/util/lp/nla_common.cpp
+++ b/src/util/lp/nla_common.cpp
@@ -28,24 +28,25 @@ 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<signed_vars>(const signed_vars& 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<signed_vars>(signed_vars 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<signed_vars>(signed_vars const& t) const;
+template lpvar common::var<smon>(smon 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<signed_vars>(const signed_vars& t) const;
+
+template rational common::canonize_sign<smon>(const smon& t) const;
 template rational common::canonize_sign<factor>(const factor& t) const;
 rational common::canonize_sign(lpvar j) const {
     return c().canonize_sign_of_var(j);
@@ -99,17 +100,17 @@ std::ostream& common::print_product(const T & m, std::ostream& out) const {
 template 
 std::ostream& common::print_product<monomial>(const monomial & m, std::ostream& out) const;
 
-template std::ostream& common::print_product<signed_vars>(const signed_vars & m, std::ostream& out) const;
+template std::ostream& common::print_product<smon>(const smon & m, std::ostream& out) const;
 
 
 std::ostream& common::print_monomial(const monomial & m, std::ostream& out) const {
     return c().print_monomial(m, out);
 }
 
-//std::ostream& common::print_rooted_monomial(const signed_vars& rm, std::ostream& out) const {
+//std::ostream& common::print_rooted_monomial(const smon& rm, std::ostream& out) const {
 //    return c().print_rooted_monomial(rm, out);
 //}
-//std::ostream& common::print_rooted_monomial_with_vars(const signed_vars& rm, std::ostream& out) const {
+//std::ostream& common::print_rooted_monomial_with_vars(const smon& rm, std::ostream& out) const {
 //        return c().print_rooted_monomial_with_vars(rm, out);
 //}
 std::ostream& common::print_factor(const factor & f, std::ostream& out) const {
diff --git a/src/util/lp/nla_common.h b/src/util/lp/nla_common.h
index 00665fe67..668acd6a5 100644
--- a/src/util/lp/nla_common.h
+++ b/src/util/lp/nla_common.h
@@ -84,8 +84,8 @@ struct common {
     std::ostream& print_var(lpvar, std::ostream& out) const;
     
     std::ostream& print_monomial(const monomial & m, std::ostream& out) const;
-    std::ostream& print_rooted_monomial(const signed_vars &, std::ostream& out) const;
-    std::ostream& print_rooted_monomial_with_vars(const signed_vars&, 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;
     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 198260903..bb07d60dc 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -97,13 +97,10 @@ rational core::canonize_sign_of_var(lpvar j) const {
     return m_evars.find(j).rsign();        
 }
     
-rational core::canonize_sign(const signed_vars& m) const {
-    NOT_IMPLEMENTED_YET();
-    return rational::one();
+rational core::canonize_sign(const smon& m) const {
+    return m.rsign();
 }
 
-    
-// returns the monomial index
 void core::add(lpvar v, unsigned sz, lpvar const* vs) {
     m_emons.add(v, sz, vs);
 }
@@ -139,7 +136,7 @@ void core::explain(const monomial& m, lp::explanation& exp) const {
         explain(j, exp);
 }
 
-void core::explain(const signed_vars& rm, lp::explanation& exp) const {
+void core::explain(const smon& rm, lp::explanation& exp) const {
     explain(m_emons[rm.var()], exp);
 }
 
@@ -165,7 +162,7 @@ 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<signed_vars>(const signed_vars & 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()) {
@@ -781,12 +778,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));
-    signed_vars const* sv = m_emons.find_canonical(vars);
+    smon 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 {
-    signed_vars const* sv = m_emons.find_canonical(vars);
+    smon const* sv = m_emons.find_canonical(vars);
     return sv ? &m_emons[sv->var()] : nullptr;
 }
 
@@ -809,7 +806,7 @@ void core::explain_separation_from_zero(lpvar j) {
         explain_existing_upper_bound(j);
 }
 
-int core::get_derived_sign(const signed_vars& rm, const factorization& f) const {
+int core::get_derived_sign(const smon& 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) {
@@ -821,7 +818,7 @@ int core::get_derived_sign(const signed_vars& rm, const factorization& f) const
     }
     return nla::rat_sign(sign);
 }
-void core::trace_print_monomial_and_factorization(const signed_vars& rm, const factorization& f, std::ostream& out) const {
+void core::trace_print_monomial_and_factorization(const smon& rm, const factorization& f, std::ostream& out) const {
     out << "rooted vars: ";
     print_product(rm.vars(), out);
     out << "\n";
@@ -1410,7 +1407,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);
-            signed_vars const* sv = m_emons.find_canonical(vv);
+            smon const* sv = m_emons.find_canonical(vv);
             if (!sv) {
                 out << "nf length" << vv.size() << "\n"; ;
             }
@@ -1439,7 +1436,7 @@ void core::init_to_refine() {
     
     TRACE("nla_solver", 
           tout << m_to_refine.size() << " mons to refine:\n";
-          for (lpvar v : m_to_refine) tout << m_emons[v] << "\n";);
+          for (lpvar v : m_to_refine) tout << pp_mon(*this, m_emons[v]) << "\n";);
 }
         
 std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
@@ -1465,7 +1462,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
     return vars;
 }
 
-bool core::divide(const signed_vars& bc, const factor& c, factor & b) const {
+bool core::divide(const smon& bc, const factor& c, factor & b) const {
     svector<lpvar> c_vars = sorted_vars(c);
     TRACE("nla_solver_div",
           tout << "c_vars = ";
@@ -1482,7 +1479,7 @@ bool core::divide(const signed_vars& bc, const factor& c, factor & b) const {
         b = factor(b_vars[0], factor_type::VAR);
         return true;
     }
-    signed_vars const* sv = m_emons.find_canonical(b_vars);
+    smon const* sv = m_emons.find_canonical(b_vars);
     if (!sv) {
         TRACE("nla_solver_div", tout << "not in rooted";);
         return false;
@@ -1532,10 +1529,10 @@ void core::print_specific_lemma(const lemma& l, std::ostream& out) const {
 }
     
 
-void core::trace_print_ol(const signed_vars& ac,
+void core::trace_print_ol(const smon& ac,
                           const factor& a,
                           const factor& c,
-                          const signed_vars& bc,
+                          const smon& bc,
                           const factor& b,
                           std::ostream& out) {
     out << "ac = " << ac << "\n";
@@ -1584,7 +1581,7 @@ std::unordered_map<unsigned, unsigned_vector> core::get_rm_by_arity() {
 
     
 
-bool core::rm_check(const signed_vars& rm) const {
+bool core::rm_check(const smon& rm) const {
     return check_monomial(m_emons[rm.var()]);
 }
     
@@ -1642,7 +1639,7 @@ void core::add_abs_bound(lpvar v, llc cmp, rational const& bound) {
 */
 
     
-bool core::find_bfc_to_refine_on_rmonomial(const signed_vars& rm, bfc & bf) {
+bool core::find_bfc_to_refine_on_rmonomial(const smon& rm, bfc & bf) {
     for (auto factorization : factorization_factory_imp(rm, *this)) {
         if (factorization.size() == 2) {
             auto a = factorization[0];
@@ -1656,7 +1653,7 @@ bool core::find_bfc_to_refine_on_rmonomial(const signed_vars& rm, bfc & bf) {
     return false;
 }
     
-bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const signed_vars*& rm_found){
+bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const smon*& rm_found){
     rm_found = nullptr;
     for (unsigned i: m_to_refine) {
         const auto& rm = m_emons.canonical[i];
@@ -1975,7 +1972,6 @@ lbool core::test_check(
     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 3b72f85b9..69e5f1c01 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(signed_vars const& sv) const { return sv.var(); }
+    lpvar var(smon const& sv) const { return sv.var(); }
 
-    rational vvr(const signed_vars& rm) const { return vvr(m_emons[rm.var()]); } // NB: removed multiplication with sign.
+    rational vvr(const smon& rm) const { return rm.rsign()*vvr(m_emons[rm.var()]); }
 
     rational vvr(const factor& f) const {  return f.is_var()? vvr(f.var()) : vvr(m_emons[f.var()]); }
 
@@ -112,7 +112,7 @@ public:
 
     svector<lpvar> sorted_vars(const factor& f) const;
     bool done() const;
-    
+
     void add_empty_lemma();
     // the value of the factor is equal to the value of the variable multiplied
     // by the canonize_sign
@@ -120,12 +120,12 @@ public:
 
     rational canonize_sign_of_var(lpvar j) const;
     
-    // the value of the rooted monomias is equal to the value of the variable multiplied
+    // 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 signed_vars& m) const;
+    rational canonize_sign(const smon& m) const;
     
 
-    void deregister_monomial_from_signed_varsomials (const monomial & m, unsigned i);
+    void deregister_monomial_from_smonomials (const monomial & m, unsigned i);
 
     void deregister_monomial_from_tables(const monomial & m, unsigned i);
 
@@ -142,7 +142,7 @@ public:
     bool check_monomial(const monomial& m) const;
     
     void explain(const monomial& m, lp::explanation& exp) const;
-    void explain(const signed_vars& rm, 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 +169,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 signed_vars& rm, const factorization& f, std::ostream& out) const;
+    void trace_print_monomial_and_factorization(const smon& 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 +177,10 @@ public:
     void print_specific_lemma(const lemma& l, std::ostream& out) const;
     
 
-    void trace_print_ol(const signed_vars& ac,
+    void trace_print_ol(const smon& ac,
                         const factor& a,
                         const factor& c,
-                        const signed_vars& bc,
+                        const smon& bc,
                         const factor& b,
                         std::ostream& out);
 
@@ -243,7 +243,7 @@ public:
     const monomial* find_monomial_of_vars(const svector<lpvar>& vars) const;
 
 
-    int get_derived_sign(const signed_vars& rm, const factorization& f) const;
+    int get_derived_sign(const smon& rm, const factorization& f) const;
 
 
     bool var_has_positive_lower_bound(lpvar j) const;
@@ -312,7 +312,7 @@ public:
 
     void init_to_refine();
 
-    bool divide(const signed_vars& bc, const factor& c, factor & b) const;
+    bool divide(const smon& bc, const factor& c, factor & b) const;
 
     void negate_factor_equality(const factor& c, const factor& d);
     
@@ -320,15 +320,15 @@ public:
 
     std::unordered_set<lpvar> collect_vars(const lemma& l) const;
 
-    bool rm_check(const signed_vars&) const;
+    bool rm_check(const smon&) 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 signed_vars& rm, bfc & bf);
+    bool  find_bfc_to_refine_on_rmonomial(const smon& rm, bfc & bf);
     
-    bool  find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const signed_vars*& rm_found);
+    bool  find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const smon*& 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 c531e88b0..0e93582bf 100644
--- a/src/util/lp/nla_monotone_lemmas.cpp
+++ b/src/util/lp/nla_monotone_lemmas.cpp
@@ -33,13 +33,13 @@ void monotone::print_monotone_array(const vector<std::pair<std::vector<rational>
     }
     out <<  "}";
 }
-bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm) {
+bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& 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 signed_vars& rmk = c().m_emons.canonical[p.second];
+        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;);
@@ -61,14 +61,14 @@ bool monotone::monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<
     return false;
 }
 
-bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm) {
+bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& 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 signed_vars& rmk = c().m_emons.canonical[p.second];
+        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;);
@@ -92,14 +92,14 @@ bool monotone::monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<
     return false;
 }
 
-bool monotone::monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm) {
+bool monotone::monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& 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 vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted) {
     for (unsigned i = 0; i < lex_sorted.size(); i++) {
         unsigned rmi = lex_sorted[i].second;
-        const signed_vars& rm = c().m_emons.canonical[rmi];
+        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;
@@ -107,7 +107,7 @@ bool monotone::monotonicity_lemma_on_lex_sorted(const vector<std::pair<std::vect
     return false;
 }
 
-vector<std::pair<rational, lpvar>> monotone::get_sorted_key_with_vars(const signed_vars& a) const {
+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.vars()) {
         r.push_back(std::make_pair(abs(vvr(j)), j));
@@ -137,8 +137,8 @@ void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) {
 }
 
 // strict version
-void monotone::generate_monl_strict(const signed_vars& a,
-                                const signed_vars& b,
+void monotone::generate_monl_strict(const smon& a,
+                                const smon& b,
                                 unsigned strict) {
     add_empty_lemma();
     auto akey = get_sorted_key_with_vars(a);
@@ -159,8 +159,8 @@ void monotone::generate_monl_strict(const signed_vars& a,
 }
 
 void monotone::assert_abs_val_a_le_abs_var_b(
-    const signed_vars& a,
-    const signed_vars& b,
+    const smon& a,
+    const smon& b,
     bool strict) {
     lpvar aj = var(a);
     lpvar bj = var(b);
@@ -188,8 +188,8 @@ void monotone::negate_abs_a_lt_abs_b(lpvar a, lpvar b) {
 
 
 // not a strict version
-void monotone::generate_monl(const signed_vars& a,
-                         const signed_vars& b) {
+void monotone::generate_monl(const smon& a,
+                         const smon& b) {
     TRACE("nla_solver", 
           tout << "a = " << a << "\n:";
           tout << "b = " << b << "\n:";);
@@ -206,7 +206,7 @@ void monotone::generate_monl(const signed_vars& a,
     TRACE("nla_solver", print_lemma(tout););
 }
 
-std::vector<rational> monotone::get_sorted_key(const signed_vars& rm) const {
+std::vector<rational> monotone::get_sorted_key(const smon& rm) const {
     std::vector<rational> r;
     for (unsigned j : rm.vars()) {
         r.push_back(abs(vvr(j)));
diff --git a/src/util/lp/nla_monotone_lemmas.h b/src/util/lp/nla_monotone_lemmas.h
index a36144e2d..c46ac8b81 100644
--- a/src/util/lp/nla_monotone_lemmas.h
+++ b/src/util/lp/nla_monotone_lemmas.h
@@ -24,21 +24,21 @@ struct monotone: common {
     monotone(core *core);
     void print_monotone_array(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted,
                                   std::ostream& out) const;
-    bool monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm);
-    bool monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm);
-    bool monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const signed_vars& rm);
+    bool monotonicity_lemma_on_lex_sorted_rm_upper(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const smon& rm);
+    bool monotonicity_lemma_on_lex_sorted_rm_lower(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const smon& rm);
+    bool monotonicity_lemma_on_lex_sorted_rm(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted, unsigned i, const smon& rm);
     bool monotonicity_lemma_on_lex_sorted(const vector<std::pair<std::vector<rational>, unsigned>>& lex_sorted);
     bool  monotonicity_lemma_on_rms_of_same_arity(const unsigned_vector& rms);
     void monotonicity_lemma();
     void monotonicity_lemma(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 signed_vars& a, const signed_vars& b,  unsigned strict);
-    void generate_monl(const signed_vars& a, const signed_vars& b);
-    std::vector<rational> get_sorted_key(const signed_vars& rm) const;
-    vector<std::pair<rational, lpvar>> get_sorted_key_with_vars(const signed_vars& a) const;
+    void 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;
     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 signed_vars& a, const signed_vars& b, bool strict);
+    void assert_abs_val_a_le_abs_var_b(const smon& a, const smon& b, bool strict);
 };
 }
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index 3c6fce009..ae1c7bce7 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -29,10 +29,10 @@ namespace nla {
 // a >< b && c < 0  => ac <> bc
 // ac[k] plays the role of c   
 
-bool order::order_lemma_on_ac_and_bc(const signed_vars& rm_ac,
+bool order::order_lemma_on_ac_and_bc(const smon& rm_ac,
                                      const factorization& ac_f,
                                      unsigned k,
-                                     const signed_vars& rm_bd) {
+                                     const smon& rm_bd) {
     TRACE("nla_solver", 
           tout << "rm_ac = " << rm_ac << "\n";
           tout << "rm_bd = " << rm_bd << "\n";
@@ -44,7 +44,7 @@ bool order::order_lemma_on_ac_and_bc(const signed_vars& rm_ac,
         order_lemma_on_ac_and_bc_and_factors(rm_ac, ac_f[(k + 1) % 2], ac_f[k], rm_bd, b);
 }
 
-bool order::order_lemma_on_ac_explore(const signed_vars& rm, const factorization& ac, unsigned k) {
+bool order::order_lemma_on_ac_explore(const smon& rm, const factorization& ac, unsigned k) {
     const factor c = ac[k];
     TRACE("nla_solver", tout << "c = "; _().print_factor_with_vars(c, tout); );
     if (c.is_var()) {
@@ -65,7 +65,7 @@ bool order::order_lemma_on_ac_explore(const signed_vars& rm, const factorization
     return false;
 }
 
-void order::order_lemma_on_factorization(const signed_vars& rm, const factorization& ab) {
+void order::order_lemma_on_factorization(const smon& rm, const factorization& ab) {
     const monomial& m = _().m_emons[rm.var()];
     TRACE("nla_solver", tout << "orig_sign = " << _().m_emons.orig_sign(rm) << "\n";);
     rational sign = _().m_emons.orig_sign(rm);
@@ -90,11 +90,11 @@ void order::order_lemma_on_factorization(const signed_vars& rm, const factorizat
 }
 // |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 signed_vars& ac,                     
+void order::generate_ol(const smon& ac,                     
                        const factor& a,
                        int c_sign,
                        const factor& c,
-                       const signed_vars& bc,
+                       const smon& bc,
                        const factor& b,
                        llc ab_cmp) {
     add_empty_lemma();
@@ -114,7 +114,7 @@ void order::generate_mon_ol(const monomial& ac,
                            lpvar a,
                            const rational& c_sign,
                            lpvar c,
-                           const signed_vars& bd,
+                           const smon& bd,
                            const factor& b,
                            const rational& d_sign,
                            lpvar d,
@@ -142,15 +142,15 @@ void order::order_lemma() {
     unsigned start = random();
     unsigned sz = rm_ref.size();
     for (unsigned i = sz; i-- > 0 && !done(); ) {        
-        const signed_vars& rm = c().m_emons.canonical[rm_ref[(i + start) % sz]];
+        const smon& rm = c().m_emons.canonical[rm_ref[(i + start) % sz]];
         order_lemma_on_rmonomial(rm);
     }
 }
 
-bool order::order_lemma_on_ac_and_bc_and_factors(const signed_vars& ac,
+bool order::order_lemma_on_ac_and_bc_and_factors(const smon& ac,
                                                  const factor& a,
                                                  const factor& c,
-                                                 const signed_vars& bc,
+                                                 const smon& bc,
                                                  const factor& b) {
     auto cv = vvr(c); 
     int c_sign = nla::rat_sign(cv);
@@ -232,10 +232,10 @@ void order::order_lemma_on_ab(const monomial& m, const rational& sign, lpvar a,
         order_lemma_on_ab_lt(m, sign, a, b);
 }
 // a > b && c > 0 => ac > bc
-void order::order_lemma_on_rmonomial(const signed_vars& rm) {
+void order::order_lemma_on_rmonomial(const smon& rm) {
     TRACE("nla_solver_details",
           tout << "rm = "; print_product(rm, tout);
-          tout << ", orig = " << c().m_emons[rm.var()] << "\n";
+          tout << ", orig = " << pp_mon(c(), c().m_emons[rm.var()]);
           );
     for (auto ac : factorization_factory_imp(rm, c())) {
         if (ac.size() != 2)
@@ -267,7 +267,7 @@ void order::order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, i
     TRACE("nla_solver", print_lemma(tout););
 }
 void order::order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const monomial& bd) {
-    signed_vars const& rm_bd = _().m_emons.canonical[bd];
+    smon const& rm_bd = _().m_emons.canonical[bd];
     factor d(_().m_evars.find(ac[k]).var(), factor_type::VAR);
     factor b;
     if (_().divide(rm_bd, d, b)) {
@@ -275,7 +275,7 @@ void order::order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, co
     }
 }
 
-void order::order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const signed_vars& bd, const factor& b, lpvar d) {
+void order::order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const smon& bd, const factor& b, lpvar d) {
     TRACE("nla_solver",  tout << "ac=" << pp_mon(c(), ac);
           tout << "\nrm=" << bd;
           print_factor(b, tout << ", b="); print_var(d, tout << ", d=") << "\n";);
diff --git a/src/util/lp/nla_order_lemmas.h b/src/util/lp/nla_order_lemmas.h
index c90cd2830..1270f5c1e 100644
--- a/src/util/lp/nla_order_lemmas.h
+++ b/src/util/lp/nla_order_lemmas.h
@@ -29,23 +29,23 @@ struct order: common {
     const core& _() const { return *m_core; }
     //constructor
     order(core *c) : common(c) {}
-    bool order_lemma_on_ac_and_bc_and_factors(const signed_vars& ac,
+    bool order_lemma_on_ac_and_bc_and_factors(const smon& ac,
                                               const factor& a,
                                               const factor& c,
-                                              const signed_vars& bc,
+                                              const smon& 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 signed_vars& rm_ac,
+    bool order_lemma_on_ac_and_bc(const smon& rm_ac,
                                   const factorization& ac_f,
                                   unsigned k,
-                                  const signed_vars& rm_bd);
+                                  const smon& rm_bd);
     
-    bool order_lemma_on_ac_explore(const signed_vars& rm, const factorization& ac, unsigned k);
+    bool order_lemma_on_ac_explore(const smon& rm, const factorization& ac, unsigned k);
 
-    void order_lemma_on_factorization(const signed_vars& rm, const factorization& ab);
+    void order_lemma_on_factorization(const smon& rm, const factorization& ab);
     
     /**
        \brief Add lemma: 
@@ -63,19 +63,19 @@ struct order: common {
     void order_lemma_on_ab(const monomial& m, const rational& sign, lpvar a, lpvar b, bool gt);
     void order_lemma_on_factor_binomial_explore(const monomial& m, unsigned k);
     void order_lemma_on_factor_binomial_rm(const monomial& ac, unsigned k, const monomial& bd);
-    void order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const signed_vars& bd, const factor& b, lpvar d);
+    void order_lemma_on_binomial_ac_bd(const monomial& ac, unsigned k, const smon& bd, const factor& b, lpvar d);
     void order_lemma_on_binomial_k(const monomial& m, lpvar k, bool gt);
     void order_lemma_on_binomial_sign(const monomial& ac, lpvar x, lpvar y, int sign);
     void order_lemma_on_binomial(const monomial& ac);
-    void order_lemma_on_rmonomial(const signed_vars& rm);
+    void order_lemma_on_rmonomial(const smon& rm);
     void order_lemma();
     // |c_sign| = 1, and c*c_sign > 0
     // ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
-    void generate_ol(const signed_vars& ac,                     
+    void generate_ol(const smon& ac,                     
                      const factor& a,
                      int c_sign,
                      const factor& c,
-                     const signed_vars& bc,
+                     const smon& bc,
                      const factor& b,
                      llc ab_cmp);
 
@@ -83,7 +83,7 @@ struct order: common {
                          lpvar a,
                          const rational& c_sign,
                          lpvar c,
-                         const signed_vars& bd,
+                         const smon& 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 b1f6e1ed8..f7d428992 100644
--- a/src/util/lp/nla_tangent_lemmas.cpp
+++ b/src/util/lp/nla_tangent_lemmas.cpp
@@ -33,7 +33,7 @@ std::ostream& tangents::print_tangent_domain(const point &a, const point &b, std
     out << "("; print_point(a, out);  out <<  ", "; print_point(b, out); out <<  ")";
     return out;
 }
-void tangents::generate_simple_tangent_lemma(const signed_vars* rm) {
+void tangents::generate_simple_tangent_lemma(const smon* rm) {
     if (rm->size() != 2)
         return;
     TRACE("nla_solver", tout << "rm:" << *rm << std::endl;);
@@ -73,7 +73,7 @@ void tangents::tangent_lemma() {
     bfc bf;
     lpvar j;
     rational sign;
-    const signed_vars* rm = nullptr;
+    const smon* rm = nullptr;
         
     if (c().find_bfc_to_refine(bf, j, sign, rm)) {
         tangent_lemma_bf(bf, j, sign, rm);
@@ -84,7 +84,7 @@ void tangents::tangent_lemma() {
     }
 }
 
-void tangents::generate_explanations_of_tang_lemma(const signed_vars& rm, const bfc& bf, lp::explanation& exp) {
+void tangents::generate_explanations_of_tang_lemma(const smon& 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);
@@ -112,7 +112,7 @@ void tangents::generate_tang_plane(const rational & a, const rational& b, const
     t.add_coeff_var( j_sign, j);
     c().mk_ineq(t, sbelow? llc::GT : llc::LT, - a*b);
 }  
-void tangents::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const signed_vars* rm){
+void tangents::tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const smon* 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 e4a116c9c..d2b4e4b84 100644
--- a/src/util/lp/nla_tangent_lemmas.h
+++ b/src/util/lp/nla_tangent_lemmas.h
@@ -47,13 +47,13 @@ struct tangents: common {
     
     tangents(core *core);
 
-    void generate_simple_tangent_lemma(const signed_vars* rm);
+    void generate_simple_tangent_lemma(const smon* rm);
     
     void tangent_lemma();
 
-    void generate_explanations_of_tang_lemma(const signed_vars& rm, const bfc& bf, lp::explanation& exp);
+    void generate_explanations_of_tang_lemma(const smon& rm, const bfc& bf, lp::explanation& exp);
     
-    void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const signed_vars* rm);
+    void tangent_lemma_bf(const bfc& bf, lpvar j, const rational& sign, const smon* 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/var_eqs.h b/src/util/lp/var_eqs.h
index f7469ba54..7f0ef16e4 100644
--- a/src/util/lp/var_eqs.h
+++ b/src/util/lp/var_eqs.h
@@ -123,6 +123,13 @@ public:
         signed_var sv = find(signed_var(j, false));
         return sv.var() == j;            
     }
+    inline bool is_root(svector<lpvar> v) const {
+        for (lpvar j : v)
+            if (! is_root(j))
+                return false;
+        return true;
+    }
+
     bool vars_are_equiv(lpvar j, lpvar k) const {
         signed_var sj = find(signed_var(j, false));
         signed_var sk = find(signed_var(k, false));