diff --git a/src/util/lp/emonomials.cpp b/src/util/lp/emonomials.cpp
index b1dec694f..5434ef6b0 100644
--- a/src/util/lp/emonomials.cpp
+++ b/src/util/lp/emonomials.cpp
@@ -134,26 +134,13 @@ namespace nla {
 
     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();
-        for (unsigned i = 0; i < m_var2index.size(); ++i) {
-            if (m_var2index[i] == UINT_MAX) {
-                v = i;
-                break;
-            }
-        }
-        unsigned idx = m_monomials.size();
-        m_monomials.push_back(monomial(v, vars, idx));
-        m_var2index.setx(v, idx, UINT_MAX);
-        do_canonize(m_monomials[idx]);
+        m_find_key = vars;
+        std::sort(m_find_key.begin(), m_find_key.end());
         monomial const* result = nullptr;
-        lpvar w; 
-        if (m_cg_table.find(v, w)) {
-            SASSERT(w != v);
+        lpvar w;
+        if (m_cg_table.find(UINT_MAX, w)) {
             result = &m_monomials[m_var2index[w]];
         }
-        m_var2index[v] = UINT_MAX;
-        m_monomials.pop_back();
         return result;
     }
 
diff --git a/src/util/lp/emonomials.h b/src/util/lp/emonomials.h
index c2ab6f4f6..915699141 100644
--- a/src/util/lp/emonomials.h
+++ b/src/util/lp/emonomials.h
@@ -28,7 +28,7 @@
 namespace nla {
 
 class emonomials : public var_eqs_merge_handler {
-
+    mutable svector<lpvar> m_find_key;
     /**
        \brief singly-lined cyclic list of monomial indices where variable occurs.
        Each variable points to the head and tail of the cyclic list.
@@ -52,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_monomials[em.m_var2index[v]].rvars();
+            auto const& vec = v != UINT_MAX? em.m_monomials[em.m_var2index[v]].rvars() : em.m_find_key;
             return string_hash(reinterpret_cast<char const*>(vec.c_ptr()), sizeof(lpvar)*vec.size(), 10);
         }
     };
@@ -67,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_monomials[em.m_var2index[u]].rvars();
-            auto const& vvec = em.m_monomials[em.m_var2index[v]].rvars();
+            auto const& uvec = u != UINT_MAX? em.m_monomials[em.m_var2index[u]].rvars(): em.m_find_key;
+            auto const& vvec = v != UINT_MAX? em.m_monomials[em.m_var2index[v]].rvars(): em.m_find_key;
             return uvec == vvec;
         }
     };
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index cfb77641d..ebf1c77a1 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -96,9 +96,12 @@ 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) {
-    SASSERT(m.size() == 2);
+    TRACE("nla_solver", tout << "m = " <<  pp_rmon(c(), m););
+    SASSERT(m.size() == 2);    
     lpvar c = m.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);
         if (done()) {
             break;
@@ -109,7 +112,11 @@ void order::order_lemma_on_factor_binomial_explore(const monomial& m, bool k) {
 // ac is a binomial
 // create order lemma on monomials bd where d is equivalent to ac[k]
 void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const monomial& bd) {
-    TRACE("nla_solver", tout << "bd=" << pp_rmon(_(), bd) << "\n";);
+    TRACE("nla_solver",
+          tout << "ac=" << pp_rmon(_(), ac) << "\n";
+          tout << "k=" << k << "\n";
+          tout << "bd=" << pp_rmon(_(), bd) << "\n";
+          );
     factor d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR);
     factor b;
     if (c().divide(bd, d, b)) {