diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index fc58a1e05..646bbc07d 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -756,6 +756,9 @@ struct solver::imp {
         m_vars_equivalence.clear();
         collect_equivs();
         m_vars_equivalence.create_tree();
+        for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) {
+            m_vars_equivalence.register_var(j, vvr(j));
+        }
     }
 
     void register_key_mono_in_rooted_monomials(monomial_coeff const& mc, unsigned i) {
@@ -873,7 +876,9 @@ struct solver::imp {
     
     bool order_lemma_on_factor(unsigned i_mon, const factorization& f, unsigned k, int sign) {
         lpvar j = f[k];
-        for (const index_with_sign& p : m_vars_equivalence.get_equivalent_vars(j)) {
+        TRACE("nla_solver", tout << "k = " << k << ", j = " << j; );
+        for (const index_with_sign& p : m_vars_equivalence.get_equivalent_vars(j, [this](unsigned h) {return vvr(h);})) {
+            TRACE("nla_solver", tout << "p.var() = " << p.var() << ", p.sign() = " << p.sign(); );
             if (order_lemma_on_factor_and_equiv(p.m_i, i_mon, f, k, sign * p.m_sign)) {
                 return true;
             }
@@ -888,7 +893,7 @@ struct solver::imp {
             if (v.is_zero())
                 continue;
 
-            int sign = ((v.is_pos() && f.sign().is_pos()) || (v.is_neg() && f.sign().is_neg()))? 1 : -1;
+            int sign = (v.is_pos() == f.sign().is_pos())? 1 : -1;
             
             if (order_lemma_on_factor(i_mon, f, k, sign)) { 
                 return true;
diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h
index f63022faf..ec73cf78d 100644
--- a/src/util/lp/vars_equivalence.h
+++ b/src/util/lp/vars_equivalence.h
@@ -72,35 +72,32 @@ struct vars_equivalence {
     };
 
    
+    //fields
     
     // The map from the variables to m_equivs indices
     // m_tree is a spanning tree of the graph of equivs represented by m_equivs
-    std::unordered_map<unsigned, unsigned> m_tree;  
+    std::unordered_map<unsigned, unsigned>       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), that k is the parent of v
-    vector<equiv>                     m_equivs;         // all equivalences extracted from constraints
+    vector<equiv>                                m_equivs;         // all equivalences extracted from constraints
+    std::unordered_map<rational,unsigned_vector> m_vars_by_abs_values;
+
     void clear() {
         m_equivs.clear();
         m_tree.clear();
     }
     // it also returns (j, 1)
-    vector<index_with_sign> get_equivalent_vars(lpvar j) const {
-        // it is just a place holder, see if we need something more substantial
+    vector<index_with_sign> get_equivalent_vars(lpvar j, std::function<rational(lpvar)> vvr) const {
         vector<index_with_sign> ret;
-        ret.push_back(index_with_sign(j, rational(1)));
+        
+        rational val = vvr(j);
+        for (lpvar j : m_vars_by_abs_values.find(abs(val))->second) {
+            if (val.is_pos())
+                ret.push_back(index_with_sign(j, rational(1)));
+            else
+                ret.push_back(index_with_sign(j, rational(-1)));
+        }
         return ret; 
-        /*
-        vector<index_with_sign> ret;
-        std::unordered_set<unsigned> returned;
-        std::unordered_set<unsigned> processed;
-        ret.push_back(std::make_pair(j, 1));
-        returned.insert(j);
-        processed.insert(j);
-        std::queue<unsigned> q;
-        q.enqueue(j);
-        
-        */
-        
     } 
 
     unsigned size() const { return static_cast<unsigned>(m_tree.size()); }
@@ -194,5 +191,16 @@ struct vars_equivalence {
             add_equiv_exp(j, exp);
     }
 
+    void register_var(unsigned j, const rational& val) {
+        rational v = abs(val);
+        auto it = m_vars_by_abs_values.find(v);
+        if (it == m_vars_by_abs_values.end()) {
+            unsigned_vector uv;
+            uv.push_back(j);
+            m_vars_by_abs_values[val] = uv;
+        } else {
+            it->second.push_back(j);
+        }
+    }
 }; // end of vars_equivalence
 }