diff --git a/src/util/lp/factorization.h b/src/util/lp/factorization.h
index 8337651b8..c0ad8ab62 100644
--- a/src/util/lp/factorization.h
+++ b/src/util/lp/factorization.h
@@ -49,7 +49,7 @@ public:
     }
     bool sign() const { return m_sign; }
     bool& sign() { return m_sign; }
-    rational rsign() const { return m_sign? rational(-1) : rational(1); }
+    rational rat_sign() const { return m_sign? rational(-1) : rational(1); }
 };
 
 
diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index d5f047495..b7259b25b 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -93,7 +93,7 @@ svector<lpvar> core::sorted_rvars(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.rsign() * (f.is_var()? canonize_sign_of_var(f.var()) : m_emons[f.var()].rsign());
+    return f.rat_sign() * (f.is_var()? canonize_sign_of_var(f.var()) : m_emons[f.var()].rsign());
 }
 
 rational core::canonize_sign_of_var(lpvar j) const {
diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h
index 06b3e996e..c39016c1e 100644
--- a/src/util/lp/nla_core.h
+++ b/src/util/lp/nla_core.h
@@ -106,7 +106,7 @@ public:
 
     rational val_rooted(const monomial& m) const { return m.rsign()*val(m.var()); }
 
-    rational val(const factor& f) const {  return f.rsign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); }
+    rational val(const factor& f) const {  return f.rat_sign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); }
 
     lpvar var(const factor& f) const { return f.var(); }
 
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index bdfb7812e..b474c490e 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -180,7 +180,7 @@ void order::generate_mon_ol(const monomial& ac,
     add_empty_lemma();
     mk_ineq(c_sign, c, llc::LE);
     explain(c); // this explains c == +- d
-    mk_ineq(c_sign, a, -d_sign, b.var(), negate(ab_cmp));
+    mk_ineq(c_sign, a, -d_sign * b.rat_sign(), b.var(), negate(ab_cmp));
     mk_ineq(ac.var(), rational(-1), var(bd), ab_cmp);
     explain(bd);
     explain(b);