diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 040f754ef..6975c972a 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1,4 +1,4 @@
- /*++
+/*++
 Copyright (c) 2017 Microsoft Corporation
 
 Module Name:
@@ -88,6 +88,13 @@ lpvar core::map_to_root(lpvar j) const {
     return m_evars.find(j).var();
 }
     
+// Reduce a single variable to its root and provide the reduction sign.
+lpvar core::reduce_var_to_rooted(lpvar j, rational & sign) const {
+    auto root = m_evars.find(j);
+    sign = rational(root.sign() ? -1 : 1);
+    return root.var();
+}
+    
 svector<lpvar> core::sorted_rvars(const factor& f) const {
     if (f.is_var()) {
         svector<lpvar> r; r.push_back(map_to_root(f.var()));
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index e06faafff..684b58d01 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -281,8 +281,12 @@ public:
 
     svector<lpvar> reduce_monic_to_rooted(const svector<lpvar> & vars, rational & sign) const;
 
-    monic_coeff canonize_monic(monic const& m) const;
+    // Reduce a single variable to its canonical root under current equalities
+    // and return the convertion 	sign as either 1 or -1
+    lpvar reduce_var_to_rooted(lpvar v, rational & sign) const;
 
+    monic_coeff canonize_monic(monic const& m) const;
+    
     int vars_sign(const svector<lpvar>& v);
     bool has_upper_bound(lpvar j) const; 
     bool has_lower_bound(lpvar j) const;
@@ -357,10 +361,6 @@ public:
     template <typename T>
     bool vars_are_roots(const T& v) const;
 
-    void register_monic_in_tables(unsigned i_mon);
-
-    void register_monics_in_tables();
-
     void clear();
     
     void init_search();
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index f25cd97e4..9e221e6ea 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -280,6 +280,7 @@ struct solver::imp {
         TRACE(nra,
               m_nlsat->display(tout << r << "\n");
               display(tout);
+              tout << "m_lp2nl:\n";
               for (auto [j, x] : m_lp2nl) tout << "j" << j << " := x" << x << "\n";);
         switch (r) {
             case l_true:
@@ -317,14 +318,19 @@ struct solver::imp {
                             case 0:
                                 bound -= coeff;
                                 break;
-                            case 1:
-                                v = nl2lp[pm.get_var(m, 0)];
-                                t.add_monomial(coeff, v);
+                            case 1: {
+                                    v = nl2lp[pm.get_var(m, 0)];
+                                    rational s;
+                                    v = m_nla_core.reduce_var_to_rooted(v, s);
+                                    t.add_monomial(s * coeff, v);
+                                }
                                 break;
                             default: {
                                 svector<lp::lpvar> vars;
                                 for (unsigned j = 0; j < num_vars; ++j)
                                     vars.push_back(nl2lp[pm.get_var(m, j)]);
+                                rational s(1);    
+                                vars = m_nla_core.reduce_monic_to_rooted(vars, s);
                                 auto mon = m_nla_core.emons().find_canonical(vars);
                                 if (mon) 
                                     v = mon->var();                                
@@ -339,12 +345,12 @@ struct solver::imp {
                                     // polynomials so punt for now.
                                     m_nla_core.add_monic(v, vars.size(), vars.data());
                                 }
-                                t.add_monomial(coeff, v);
+                                t.add_monomial(s * coeff, v);
                                 break;
                             }
                         }                      
                     }                   
-
+                    TRACE(nra, this->lra.print_term(t, tout << "t:") << std::endl;);
                     switch (a->get_kind()) {
                         case nlsat::atom::EQ: 
                             lemma |= nla::ineq(lp::lconstraint_kind::EQ, t, bound);