diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index 87faddbdd..a01e186d1 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -199,14 +199,12 @@ std::ostream& core::print_bfc(const bfc& m, std::ostream& out) const {
     return out << "( x = "; print_factor(m.m_x, out); out <<  ", y = "; print_factor(m.m_y, out); out <<  ")";
 }
 
-
 std::ostream& core::print_monomial_with_vars(lpvar v, std::ostream& out) const {
     return print_monomial_with_vars(m_emons[v], out);
 }
-
 template <typename T>
 std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const {
-    print_product(m.vars(), out) << "\n";
+    print_product(m, out) << "\n";
     for (unsigned k = 0; k < m.size(); k++) {
         print_var(m[k], out);
     }
@@ -215,9 +213,9 @@ std::ostream& core::print_product_with_vars(const T& m, std::ostream& out) const
 
 std::ostream& core::print_monomial_with_vars(const monomial& m, std::ostream& out) const {
     out << "["; print_var(m.var(), out) << "]\n";
-    for (lpvar j: m.vars())
-        print_var(j, out);
-    out << ")\n";
+    out << "vars:"; print_product_with_vars(m.vars(), out) << "\n";
+    out << "rvars:"; print_product_with_vars(m.rvars(), out) << "\n";
+    out << "rsign:" << m.rsign() << "\n";
     return out;
 }
 
diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h
index 5a40e3bb6..7537a4a45 100644
--- a/src/util/lp/nla_core.h
+++ b/src/util/lp/nla_core.h
@@ -338,30 +338,36 @@ public:
     lbool  test_check(vector<lemma>& l);
 };  // end of core
 
-    struct pp_mon {
-        core const& c;
-        monomial const& m;
-        pp_mon(core const& c, monomial const& m): c(c), m(m) {}
-        pp_mon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {}
-    };
+struct pp_mon {
+    core const& c;
+    monomial const& m;
+    pp_mon(core const& c, monomial const& m): c(c), m(m) {}
+    pp_mon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {}
+};
+struct pp_rmon {
+    core const& c;
+    monomial const& m;
+    pp_rmon(core const& c, monomial const& m): c(c), m(m) {}
+    pp_rmon(core const& c, lpvar v): c(c), m(c.m_emons[v]) {}
+};
+inline std::ostream& operator<<(std::ostream& out, pp_mon const& p) { return p.c.print_monomial(p.m, out); }
+inline std::ostream& operator<<(std::ostream& out, pp_rmon const& p) { return p.c.print_monomial_with_vars(p.m, out); }
 
-    inline std::ostream& operator<<(std::ostream& out, pp_mon const& p) { return p.c.print_monomial(p.m, out); }
+struct pp_fac {
+    core const& c;
+    factor const& f;
+    pp_fac(core const& c, factor const& f): c(c), f(f) {}
+};
 
-    struct pp_fac {
-        core const& c;
-        factor const& f;
-        pp_fac(core const& c, factor const& f): c(c), f(f) {}
-    };
+inline std::ostream& operator<<(std::ostream& out, pp_fac const& f) { return f.c.print_factor(f.f, out); }
 
-    inline std::ostream& operator<<(std::ostream& out, pp_fac const& f) { return f.c.print_factor(f.f, out); }
+struct pp_var {
+    core const& c;
+    lpvar v;
+    pp_var(core const& c, lpvar v): c(c), v(v) {}
+};
 
-    struct pp_var {
-        core const& c;
-        lpvar v;
-        pp_var(core const& c, lpvar v): c(c), v(v) {}
-    };
-
-    inline std::ostream& operator<<(std::ostream& out, pp_var const& v) { return v.c.print_var(v.v, out); }
+inline std::ostream& operator<<(std::ostream& out, pp_var const& v) { return v.c.print_var(v.v, out); }
 
 } // end of namespace nla
 
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index 87f384ed4..bf4c1d3ab 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -61,10 +61,10 @@ void order::order_lemma_on_rmonomial(const monomial& m) {
 // a > b && c > 0 => ac > bc,
 // with either variable of ac playing the role of c
 void order::order_lemma_on_binomial(const monomial& ac) {
-    TRACE("nla_solver", tout << pp_mon(c(), ac););
+    TRACE("nla_solver", tout << pp_rmon(c(), ac););
     SASSERT(!check_monomial(ac) && ac.size() == 2);
-    const rational mult_val = val(ac.vars()[0]) * val(ac.vars()[1]);
-    const rational acv = val(ac);
+    const rational mult_val = val(ac.rvars()[0]) * val(ac.rvars()[1]);
+    const rational acv = val(ac)*ac.rsign();
     bool gt = acv > mult_val;
     bool k = false;
     do {