diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 02ad786dd..ec4a5ec87 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -493,6 +493,8 @@ namespace smt {
         TRACE("lemma", tout << strm.str() << "\n";);
         display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
         out.close();
+        if (m_lemma_id==6184)
+            exit(0);
         return m_lemma_id;
     }
 
diff --git a/src/util/lp/factorization.cpp b/src/util/lp/factorization.cpp
index 48be88383..beb442791 100644
--- a/src/util/lp/factorization.cpp
+++ b/src/util/lp/factorization.cpp
@@ -14,7 +14,7 @@ void const_iterator_mon::init_vars_by_the_mask(unsigned_vector & k_vars, unsigne
         }
     }
 }
-            
+// todo : do we need the sign?
 bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const {
     unsigned_vector k_vars;
     unsigned_vector j_vars;
@@ -30,7 +30,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
         if (!m_ff->find_rm_monomial_of_vars(k_vars, i)) {
             return false;
         }
-        k.set(i, factor_type::RM);
+        k.set(i, factor_type::MON);
     }
 
     if (j_vars.size() == 1) {
@@ -40,7 +40,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
         if (!m_ff->find_rm_monomial_of_vars(j_vars, i)) {
             return false;
         }
-        j.set(i, factor_type::RM);
+        j.set(i, factor_type::MON);
     }
     return true;
 }
diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h
index 408de84dd..8337651b8 100644
--- a/src/util/lp/factorization.h
+++ b/src/util/lp/factorization.h
@@ -27,14 +27,16 @@ namespace nla {
 struct factorization_factory;
 typedef unsigned lpvar;
 
-enum class factor_type { VAR, RM }; // RM stands for rooted monomial 
+enum class factor_type { VAR, MON };
 
 class factor {
     lpvar        m_var;
     factor_type  m_type;
+    bool        m_sign;
 public:
-    factor(): m_var(UINT_MAX), m_type(factor_type::VAR) {}
-    explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t) {}
+    factor(): factor(false) {}
+    factor(bool sign): m_var(UINT_MAX), m_type(factor_type::VAR), m_sign(sign) {}
+    explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t), m_sign(false) {}
     unsigned var() const { return m_var; }
     factor_type type() const { return m_type; }
     void set(lpvar v, factor_type t) { m_var = v; m_type = t; }
@@ -45,6 +47,9 @@ public:
     bool operator!=(factor const& other) const {
         return m_var != other.var() || m_type != other.type();
     }
+    bool sign() const { return m_sign; }
+    bool& sign() { return m_sign; }
+    rational rsign() const { return m_sign? rational(-1) : rational(1); }
 };
 
 
diff --git a/src/util/lp/nla_common.cpp b/src/util/lp/nla_common.cpp
index db7c91805..d35b684b6 100644
--- a/src/util/lp/nla_common.cpp
+++ b/src/util/lp/nla_common.cpp
@@ -36,7 +36,6 @@ template <typename T> rational common::val(T const& t) const { return c().val(t)
 template rational common::val<monomial>(monomial const& t) const;
 template rational common::val<factor>(factor const& t) const;
 rational common::val(lpvar t) const { return c().val(t); }
-rational common::rval(const monomial& m) const { return c().rval(m); }
 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<monomial>(monomial const& t) const;
diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index f7aa8801e..d5f047495 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -76,10 +76,14 @@ bool core::lemma_holds(const lemma& l) const {
     }
     return false;
 }
+
+lpvar core::map_to_root(lpvar j) const {
+    return m_evars.find(j).var();
+}
     
-svector<lpvar> core::sorted_vars(const factor& f) const {
+svector<lpvar> core::sorted_rvars(const factor& f) const {
     if (f.is_var()) {
-        svector<lpvar> r; r.push_back(f.var());
+        svector<lpvar> r; r.push_back(map_to_root(f.var()));
         return r;
     }
     TRACE("nla_solver", tout << "nv";);
@@ -89,14 +93,23 @@ svector<lpvar> core::sorted_vars(const factor& f) const {
 // 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[f.var()].rsign();
+    return f.rsign() * (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();        
 }
-    
+
+bool core::canonize_sign_is_correct(const monomial& m) const {
+    rational r(1);
+    for (lpvar j : m.vars()) {
+        r *= canonize_sign_of_var(j);
+    }
+    return r == m.rsign();
+}
+
 rational core::canonize_sign(const monomial& m) const {
+    SASSERT(canonize_sign_is_correct(m));
     return m.rsign();
 }
 
@@ -157,11 +170,13 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
 }
 
 std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
+    if (f.sign())
+        out << "- ";
     if (f.is_var()) {
         out << "VAR,  ";
         print_var(f.var(), out);
     } else {
-        out << "PROD, ";
+        out << "MON, ";
         print_product(m_emons[f.var()].rvars(), out);
     }
     out << "\n";
@@ -1372,30 +1387,38 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
     return vars;
 }
 
+// divides bc by c, so bc = b*c
 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 = ";
-          print_product(c_vars, tout);
-          tout << "\nbc_vars = ";
+    svector<lpvar> c_rvars = sorted_rvars(c);
+    TRACE("nla_solver",
+          tout << "c_rvars = ";
+          print_product(c_rvars, tout);
+          tout << "\nbc_rvars = ";
           print_product(bc.rvars(), tout););
-    if (!lp::is_proper_factor(c_vars, bc.rvars()))
+    if (!lp::is_proper_factor(c_rvars, bc.rvars()))
         return false;
             
-    auto b_vars = lp::vector_div(bc.rvars(), c_vars);
-    TRACE("nla_solver_div", tout << "b_vars = "; print_product(b_vars, tout););
-    SASSERT(b_vars.size() > 0);
-    if (b_vars.size() == 1) {
-        b = factor(b_vars[0], factor_type::VAR);
-        return true;
+    auto b_rvars = lp::vector_div(bc.rvars(), c_rvars);
+    TRACE("nla_solver_div", tout << "b_rvars = "; print_product(b_rvars, tout););
+    SASSERT(b_rvars.size() > 0);
+    if (b_rvars.size() == 1) {
+        b = factor(b_rvars[0], factor_type::VAR);
+    } else {
+        monomial const* sv = m_emons.find_canonical(b_rvars);
+        if (!sv) {
+            TRACE("nla_solver_div", tout << "not in rooted";);
+            return false;
+        }
+        b = factor(sv->var(), factor_type::MON);
     }
-    monomial const* sv = m_emons.find_canonical(b_vars);
-    if (!sv) {
-        TRACE("nla_solver_div", tout << "not in rooted";);
-        return false;
-    }
-    b = factor(sv->var(), factor_type::RM);
-    TRACE("nla_solver_div", tout << "success div:"; print_factor(b, tout););
+    SASSERT(!b.sign());
+    // we should have bc.vars()*canonize_sign(bc) = bc.rvar() = b.rvars()*c.rvars() =
+    // = canonize_sign(b)*b.vars()* canonize_sign(c)*c.vars().
+    // so bc.vars()*canonize_sign(bc) = canonize_sign(b)*b.vars()* canonize_sign(c)*c.vars().
+    // but canonize_sign(b) now is canonize_sign_of_var(b.m_var) or canonize_sign(m_monomials[b.m_var])
+    // so we are adjusting it
+    b.sign() = (canonize_sign(b) * canonize_sign(c) * canonize_sign(bc) == rational(1))? false: true; 
+    TRACE("nla_solver", tout << "success div:"; print_factor(b, tout););
     return true;
 }
 
@@ -1468,8 +1491,8 @@ void core::maybe_add_a_factor(lpvar i,
         }
     } else {
         if (try_insert(i, found_rm)) {
-            r.push_back(factor(i, factor_type::RM));
-            TRACE("nla_solver", tout << "inserting factor = "; print_factor_with_vars(factor(i, factor_type::RM), tout); );
+            r.push_back(factor(i, factor_type::MON));
+            TRACE("nla_solver", tout << "inserting factor = "; print_factor_with_vars(factor(i, factor_type::MON), tout); );
         }
     }
 }
diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h
index 23965cca8..06b3e996e 100644
--- a/src/util/lp/nla_core.h
+++ b/src/util/lp/nla_core.h
@@ -100,17 +100,17 @@ public:
 
     rational val(const monomial& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
 
-    rational rval(const monomial& m) const { return val(m)*m.rsign(); }
+    bool canonize_sign_is_correct(const monomial& m) const;
 
     lpvar var(monomial const& sv) const { return sv.var(); }
 
     rational val_rooted(const monomial& m) const { return m.rsign()*val(m.var()); }
 
-    rational val(const factor& f) const {  return f.is_var()? val(f.var()) : val(m_emons[f.var()]); }
+    rational val(const factor& f) const {  return f.rsign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); }
 
     lpvar var(const factor& f) const { return f.var(); }
 
-    svector<lpvar> sorted_vars(const factor& f) const;
+    svector<lpvar> sorted_rvars(const factor& f) const;
     bool done() const;
 
     void add_empty_lemma();
@@ -338,6 +338,7 @@ public:
     bool  no_lemmas_hold() const;
     
     lbool  test_check(vector<lemma>& l);
+    lpvar map_to_root(lpvar) const;
 };  // end of core
 
 struct pp_mon {
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index ebf1c77a1..bdfb7812e 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -95,14 +95,15 @@ void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, i
 }
 
 // We look for monomials e = m.rvars()[k]*d and see if we can create an order lemma for m and  e
-void order::order_lemma_on_factor_binomial_explore(const monomial& m, bool k) {
-    TRACE("nla_solver", tout << "m = " <<  pp_rmon(c(), m););
-    SASSERT(m.size() == 2);    
-    lpvar c = m.vars()[k];
+void order::order_lemma_on_factor_binomial_explore(const monomial& ac, bool k) {
+    TRACE("nla_solver", tout << "ac = " <<  pp_rmon(c(), ac););
+    SASSERT(ac.size() == 2);    
+    lpvar c = ac.vars()[k];
     
-    for (monomial const& m2 : _().m_emons.get_products_of(c)) {
-        TRACE("nla_solver", tout << "m2 = " << pp_rmon(_(), m2););
-        order_lemma_on_factor_binomial_rm(m, k, m2);
+    for (monomial const& bd : _().m_emons.get_products_of(c)) {
+        if (bd.var() == ac.var()) continue;
+        TRACE("nla_solver", tout << "bd = " << pp_rmon(_(), bd););
+        order_lemma_on_factor_binomial_rm(ac, k, bd);
         if (done()) {
             break;
         }
@@ -118,18 +119,19 @@ void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const
           tout << "bd=" << pp_rmon(_(), bd) << "\n";
           );
     factor d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR);
-    factor b;
+    factor b(false);
     if (c().divide(bd, d, b)) {
         order_lemma_on_binomial_ac_bd(ac, k, bd, b, d.var());
     }
 }
 
-// suppose ac >= bd and |c| = |d| => then ac/|c| >= bd/|d|
+//  ac >= bd && |c| = |d| => ac/|c| >= bd/|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_rmon(_(), ac) << "\nrm= " << pp_rmon(_(), bd) << ", b= " << pp_fac(_(), b) << ", d= " << pp_var(_(), d) << "\n";);
     lpvar a = ac.vars()[!k];
     lpvar c = ac.vars()[k];
+    TRACE("nla_solver",  
+          tout << "ac = " << pp_mon(_(), ac) << "a = " << pp_var(_(), a) << "c = " << pp_var(_(), c) << "\nbd = " << pp_mon(_(), bd) << "b = " << pp_fac(_(), b) << "d = " << pp_var(_(), d) << "\n";
+          );
     SASSERT(_().m_evars.find(c).var() == d);
     rational acv = val(ac);
     rational av = val(a);
@@ -139,7 +141,10 @@ void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const mono
     rational bv = val(b);
     // Notice that ac/|c| = a*c_sign , and bd/|d| = b*d_sign
     auto av_c_s = av*c_sign; auto bv_d_s = bv*d_sign;
-
+    TRACE("nla_solver",  
+          tout << "acv = " << acv << ", av = " << av << ", c_sign = " << c_sign << ", d_sign = " << d_sign << ", bdv = " << bdv <<
+          "\nbv = " << bv << ", av_c_s = " << av_c_s << ", bv_d_s = " << bv_d_s << "\n";);
+   
     if (acv >= bdv && av_c_s < bv_d_s)
         generate_mon_ol(ac, a, c_sign, c, bd, b, d_sign, d, llc::LT);
     else if (acv <= bdv && av_c_s > bv_d_s)
@@ -198,7 +203,7 @@ bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac,
           tout << "rm_bd = " << pp_rmon(_(), rm_bd) << "\n";
           tout << "ac_f[k] = ";
           c().print_factor_with_vars(ac_f[k], tout););
-    factor b;
+    factor b(false);
     return 
         c().divide(rm_bd, ac_f[k], b) && 
         order_lemma_on_ac_and_bc_and_factors(rm_ac, ac_f[!k], ac_f[k], rm_bd, b);
@@ -218,7 +223,7 @@ void order::order_lemma_on_factorization(const monomial& m, const factorization&
     if (mv == fv)
         return;
     bool gt = mv > fv;
-    TRACE("nla_solver_f", tout << "m="; _().print_monomial_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
+    TRACE("nla_solver", tout << "m="; _().print_monomial_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
     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);
diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h
deleted file mode 100644
index ca4f51a94..000000000
--- a/src/util/lp/vars_equivalence.h
+++ /dev/null
@@ -1,251 +0,0 @@
-/*++
-  Copyright (c) 2017 Microsoft Corporation
-
-  Module Name:
-
-  <name>
-
-  Abstract:
-
-  <abstract>
-
-  Author:
-  Nikolaj Bjorner (nbjorner)
-  Lev Nachmanson (levnach)
-
-  Revision History:
-
-
-  --*/
-
-namespace nla {
-
-typedef lp::constraint_index     lpci;
-typedef lp::explanation          expl_set;
-typedef lp::var_index            lpvar;
-struct hash_svector {
-    size_t operator()(const unsigned_vector & v) const {
-        return svector_hash<unsigned_hash>()(v);
-    }
-};
-
-
-
-struct vars_equivalence {
-    
-    struct equiv {
-        lpvar                m_i;
-        lpvar                m_j;
-        rational             m_sign;
-        lpci                 m_c0;
-        lpci                 m_c1;
-
-        equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1) :
-            m_i(i),
-            m_j(j),
-            m_sign(sign),
-            m_c0(c0),
-            m_c1(c1) {
-            SASSERT(m_i != m_j);
-        }
-    };
-
-    struct node {
-        unsigned            m_parent;   // points to m_equivs
-        svector<unsigned>   m_children;  // point to m_equivs
-        node() : m_parent(-1) {}
-    };
-   
-    //fields
-    
-    // The map from the variables to m_nodes
-    // m_tree is a spanning tree of the graph of equivs represented by m_equivs
-    std::unordered_map<unsigned, node>            m_tree;  
-    // If m_tree[v] == -1 then the variable is a root.
-    // if m_tree[v] is not equal to -1 then m_equivs[m_tree[v]] = (k, v) or (v, k), where k is the parent of v
-    vector<equiv>                                 m_equivs;         // all equivalences extracted from constraints
-    std::function<rational(lpvar)>                m_val;
-    
-
-    // constructor
-    vars_equivalence(std::function<rational(lpvar)> val) : m_val(val) {}
-    
-    void clear() {
-        m_equivs.clear();
-        m_tree.clear();
-    }
-
-    // j itself is also included
-    svector<lpvar> eq_vars(lpvar j) const {
-        svector<lpvar> r = path_to_root(j);
-        r.append(children(j));
-        r.push_back(j);
-        return r;
-    } 
-
-    svector<lpvar> children(lpvar j) const {
-        svector<lpvar> r;
-        auto it = m_tree.find(j);
-        if (it == m_tree.end())
-            return r;
-
-        const node& n = it->second;
-        for (unsigned e_k: n.m_children) {
-            const equiv & e = m_equivs[e_k];
-            lpvar oj = e.m_i == j? e.m_j : e.m_i;
-            r.push_back(oj);
-            for (lpvar k :  children(oj)) {
-                r.push_back(k);
-            }
-        }
-        return r;
-    } 
-
-    
-    
-    svector<lpvar> path_to_root(lpvar j) const {
-        svector<lpvar> r;
-        while (true) {
-            auto it = m_tree.find(j);
-            if (it == m_tree.end() || it->second.m_parent == static_cast<unsigned>(-1))
-                return r;
-              
-            const equiv & e = m_equivs[it->second.m_parent];
-            j = get_parent_node(j, e);
-            r.push_back(j);
-        }
-        SASSERT(false);
-    } 
-
-    
-    unsigned size() const { return static_cast<unsigned>(m_tree.size()); }
-
-    // we create a spanning tree on all variables participating in an equivalence
-    void create_tree() {
-        for (unsigned k = 0; k < m_equivs.size(); k++)
-            connect_equiv_to_tree(k);
-    }
-
-    void add_equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1) {
-        m_equivs.push_back(equiv(i, j, sign, c0, c1));
-    }
-    
-    void connect_equiv_to_tree(unsigned k) {
-        // m_tree is the tree with the edges formed by m_equivs
-        const equiv &e = m_equivs[k];
-        TRACE("nla_vars_eq", tout << "m_i = " << e.m_i << ", " << "m_j = " << e.m_j ;);
-        auto it_i = m_tree.find(e.m_i);
-        auto it_j = m_tree.find(e.m_j);
-        bool i_is_in = it_i != m_tree.end();
-        bool j_is_in = it_j != m_tree.end();
-        
-        if (!(i_is_in || j_is_in)) {
-            // none of the edge vertices is in the tree
-            // let m_i be the parent, and m_j be the child
-            TRACE("nla_vars_eq", tout << "create nodes for " << e.m_i << " and " << e.m_j; );
-            node parent;
-            node child;
-            child.m_parent = k;
-            parent.m_children.push_back(k);
-            m_tree.emplace(e.m_i, parent);
-            m_tree.emplace(e.m_j, child);
-        } else if (i_is_in && (!j_is_in)) {
-            // create a node for m_j, with m_i is the parent
-            node child;
-            child.m_parent = k;
-            TRACE("nla_vars_eq", tout << "create a node for " << e.m_j; );
-            m_tree.emplace(e.m_j, child);
-            it_i->second.m_children.push_back(k);
-        } else if ((!i_is_in) && j_is_in) {
-            TRACE("nla_vars_eq", tout << "create a node for " << e.m_i; );
-            node child;
-            child.m_parent = k;            
-            m_tree.emplace(e.m_i, child);
-            it_j->second.m_children.push_back(k);            
-        } else {
-            TRACE("nla_vars_eq", tout << "both vertices are in the tree";);
-        }
-    }
-    
-    bool empty() const {
-        return m_tree.empty();
-    }
-
-    bool is_root(unsigned j) const {
-        auto it = m_tree.find(j);
-        if (it == m_tree.end())
-            return true;
-
-        return it->second.m_parent == static_cast<unsigned>(-1);
-    }
-
-    static unsigned get_parent_node(unsigned j, const equiv& e) {
-        SASSERT(e.m_i == j || e.m_j == j);
-        return e.m_i == j? e.m_j : e.m_i;
-    }
-
-    bool vars_are_equiv(lpvar a, lpvar b) const {
-        return map_to_root(a) == map_to_root(b);
-    }
-
-
-    // Finds the root var which is equivalent to j.
-    // The sign is flipped if needed
-    lpvar map_to_root(lpvar j, rational& sign) const {
-        TRACE("nla_vars_eq", tout << "j = " << j << "\n";);
-        while (true) {
-            auto it = m_tree.find(j);
-            if (it == m_tree.end())
-                return j;
-            if (it->second.m_parent == static_cast<unsigned>(-1)) {
-                TRACE("nla_vars_eq", tout << "mapped to " << j << "\n";);
-                return j;
-            }
-            const equiv & e = m_equivs[it->second.m_parent];
-            sign *= e.m_sign;
-            j = get_parent_node(j, e);
-        }
-    }
-
-        // Finds the root var which is equivalent to j.
-    // The sign is flipped if needed
-    lpvar map_to_root(lpvar j) const {
-        while (true) {
-            auto it = m_tree.find(j);
-            if (it == m_tree.end())
-                return j;
-            if (it->second.m_parent == static_cast<unsigned>(-1))
-                return j;
-            const equiv & e = m_equivs[it->second.m_parent];
-            j = get_parent_node(j, e);
-        }
-    }
-
-    template <typename T>
-    void explain(const T& collection, expl_set & exp) const {
-        for (lpvar j : collection) {
-            explain(j, exp);
-        }
-    } 
-    void explain(lpvar j, expl_set& exp) const {
-        while (true) {
-            auto it = m_tree.find(j);
-            if (it == m_tree.end())
-                return;
-            if (it->second.m_parent == static_cast<unsigned>(-1))
-                return;
-            const equiv & e = m_equivs[it->second.m_parent];
-            exp.add(e.m_c0);
-            exp.add(e.m_c1);
-            j = get_parent_node(j, e);
-        }
-    }
-    
-    template <typename T>
-    void add_explanation_of_reducing_to_rooted_monomial(const T & m, expl_set & exp) const {
-        for (lpvar j : m)
-            explain(j, exp);
-    }
-
-}; // end of vars_equivalence
-}