diff --git a/src/util/lp/nla_basics_lemmas.cpp b/src/util/lp/nla_basics_lemmas.cpp
index d627197b9..b5bf55f01 100644
--- a/src/util/lp/nla_basics_lemmas.cpp
+++ b/src/util/lp/nla_basics_lemmas.cpp
@@ -703,7 +703,7 @@ void basics::basic_lemma_for_mon_neutral_model_based(const monomial& rm, const f
 // 1 * 1 ... * 1 * x * 1 ... * 1 = x
 bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(const monomial& rm, const factorization& f) {
     rational sign = sign_to_rat(rm.rsign());
-    TRACE("nla_solver_bl", tout << "f = "; c().print_factorization(f, tout); tout << ", sign = " << sign << '\n'; );
+    TRACE("nla_solver_bl", tout << pp_rmon(_(), rm) <<"\nf = "; c().print_factorization(f, tout); tout << "sign = " << sign << '\n'; );
     lpvar not_one = -1;
     for (auto j : f){
         TRACE("nla_solver_bl", tout << "j = "; c().print_factor_with_vars(j, tout););
@@ -729,7 +729,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
     if (not_one + 1) {
         // we found the only not_one
         if (val(rm) == val(not_one) * sign) {
-            TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;);
+            TRACE("nla_solver", tout << "the whole is equal to the factor" << std::endl;);
             return false;
         }
     } else {
@@ -746,7 +746,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monomial_model_based(co
     for (auto j : f){
         lpvar var_j = var(j);
         if (not_one == var_j) continue;
-        c().mk_ineq(var_j, llc::NE, j.is_var()? val(j) : c().canonize_sign(j) * val(j));   
+        c().mk_ineq(var_j, llc::NE, j.is_var()? val(j) : sign_to_rat(c().canonize_sign(j)) * val(j));   
     }
 
     if (not_one == static_cast<lpvar>(-1)) {
diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index a8b8af41b..cb30b559d 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -228,8 +228,12 @@ 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";
     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";
+    if (m.vars() == m.rvars())
+        out << "same rvars, and m.rsign = " << m.rsign() << " of course\n";
+    else {
+        out << "rvars:"; print_product_with_vars(m.rvars(), out) << "\n";
+        out << "rsign:" << m.rsign() << "\n";
+    }
     return out;
 }
 
@@ -1586,7 +1590,7 @@ bool core::find_bfc_to_refine(bfc& bf, lpvar &j, rational& sign, const monomial*
         rm_found = &rm;
         if (find_bfc_to_refine_on_rmonomial(rm, bf)) {
             j = rm.var();
-            sign = rm.rsign();
+            sign = sign_to_rat(rm.rsign());
             TRACE("nla_solver", tout << "found bf";
                   tout << ":rm:" << pp_rmon(*this, rm) << "\n";
                   tout << "bf:"; print_bfc(bf, tout);
diff --git a/src/util/lp/nla_order_lemmas.cpp b/src/util/lp/nla_order_lemmas.cpp
index 8f521f684..f3ced5bc0 100644
--- a/src/util/lp/nla_order_lemmas.cpp
+++ b/src/util/lp/nla_order_lemmas.cpp
@@ -218,7 +218,7 @@ void order::order_lemma_on_factorization(const monomial& m, const factorization&
     for (factor f: ab)
         sign ^= _().canonize_sign(f);
     const rational fv = val(ab[0]) * val(ab[1]);
-    const rational mv = sign * val(m);
+    const rational mv = sign_to_rat(sign) * val(m);
     TRACE("nla_solver",
           tout << "ab.size()=" << ab.size() << "\n";
           tout << "we should have sign*val(m):" << mv << "=(" << sign << ")*(" << val(m) <<") to be equal to " << " val(ab[0])*val(ab[1]):" << fv << "\n";);
@@ -266,7 +266,7 @@ void order::generate_ol(const monomial& ac,
                        llc ab_cmp) {
     add_empty_lemma();
     rational rc_sign = rational(c_sign);
-    mk_ineq(rc_sign * canonize_sign(c), var(c), llc::LE);
+    mk_ineq(rc_sign * sign_to_rat(canonize_sign(c)), var(c), llc::LE);
     mk_ineq(canonize_sign(ac), var(ac), !canonize_sign(bc), var(bc), ab_cmp);
     mk_ineq(sign_to_rat(canonize_sign(a))*rc_sign, var(a), - sign_to_rat(canonize_sign(b))*rc_sign, var(b), negate(ab_cmp));
     explain(ac);
diff --git a/src/util/rational.h b/src/util/rational.h
index 751d395db..0c5c6b9e2 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -137,7 +137,16 @@ public:
         m().set(m_val, r.m_val);
         return *this;
     }
+private:
+    rational & operator=(bool) {
+        UNREACHABLE(); return *this;
+    }
+    inline rational operator*(bool  r1) const {
+        UNREACHABLE();
+        return *this;
+    }
 
+public:
     rational & operator=(int v) {
         *this = rational(v);
         return *this;
@@ -506,9 +515,18 @@ inline rational operator*(rational const & r1, rational const & r2) {
     return rational(r1) *= r2; 
 }
 
+inline rational operator*(rational const & r1, bool r2) {
+    UNREACHABLE();
+    return r1 * rational(r2);
+}
 inline rational operator*(rational const & r1, int r2) {
     return r1 * rational(r2);
 }
+inline rational operator*(bool  r1, rational const & r2) {
+    UNREACHABLE();
+    return rational(r1) * r2;
+}
+
 inline rational operator*(int  r1, rational const & r2) {
     return rational(r1) * r2;
 }
@@ -521,6 +539,11 @@ inline rational operator/(rational const & r1, int r2) {
     return r1 / rational(r2);
 }
 
+inline rational operator/(rational const & r1, bool r2) {
+    UNREACHABLE();
+    return r1 / rational(r2);
+}
+
 inline rational operator/(int r1, rational const &    r2) {
     return rational(r1) / r2;
 }