diff --git a/src/math/lp/monic.h b/src/math/lp/monic.h
index 6add1719b..884adaaf8 100644
--- a/src/math/lp/monic.h
+++ b/src/math/lp/monic.h
@@ -77,6 +77,8 @@ public:
     
     svector<lpvar>::const_iterator begin() const { return vars().begin(); }
     svector<lpvar>::const_iterator end() const { return vars().end(); }
+
+    rational rat_sign() const { return m_rsign ? rational(-1) : rational(1); }
 };
 
 inline std::ostream& operator<<(std::ostream& out, monic const& m) {
diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index 090cd0e6c..8f00d8449 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -262,7 +262,7 @@ void order::generate_ol_eq(const monic& ac,
     // ac == bc
     lemma |= ineq(c.var(), llc::EQ, 0); // c is not equal to zero
     lemma |= ineq(term(ac.var(), -rational(1), bc.var()), llc::NE, 0);
-    lemma |= ineq(term(sign_to_rat(canonize_sign(a)), a.var(), sign_to_rat(!canonize_sign(b)), b.var()), llc::EQ, 0);
+    lemma |= ineq(term(a.rat_sign(), a.var(), -b.rat_sign(), b.var()), llc::EQ, 0);
     lemma &= ac;
     lemma &= a;
     lemma &= bc;
@@ -288,8 +288,8 @@ void order::generate_ol(const monic& ac,
     // c < 0 and ac >= bc => a <= b
     // c < 0 and ac <= bc => a >= b
     lemma |= ineq(c.var(), val(c.var()).is_neg() ? llc::GE : llc::LE, 0);
-    lemma |= ineq(term(ac.var(), -rational(1), bc.var()), val(ac.var()) < val(bc.var()) ? llc::GT : llc::LT, 0);
-    lemma |= ineq(term(a.var(),  -rational(1), b.var()),  val(a.var())  < val(b.var())  ? llc::GE : llc::LE, 0);
+    lemma |= ineq(term(rational(1), ac.var(), -rational(1), bc.var()), var_val(ac) < var_val(bc) ? llc::GT : llc::LT, 0);
+    lemma |= ineq(term(a.rat_sign(), a.var(),  -b.rat_sign(), b.var()),  val(a)  < val(b)  ? llc::GE : llc::LE, 0);
 
     lemma &= ac;
     lemma &= a;
@@ -311,10 +311,6 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
     rational c_sign = rational(nla::rat_sign(val(c)));
     auto av_c_s = val(a) * c_sign;
     auto bv_c_s = val(b) * c_sign;      
-    if (b.sign() != a.sign())
-        return false;
-    if (bc.rsign() != ac.rsign())
-        return false;
     if ((var_val(ac) > var_val(bc) && av_c_s < bv_c_s) ||
         (var_val(ac) < var_val(bc) && av_c_s > bv_c_s)) {
         generate_ol(ac, a, c, bc, b);
diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp
index 55d1dd877..35b0e5b70 100644
--- a/src/sat/smt/bv_delay_internalize.cpp
+++ b/src/sat/smt/bv_delay_internalize.cpp
@@ -179,7 +179,7 @@ namespace bv {
                 args[i] = n->get_arg(i);                
                 add_unit(eq_internalize(r, arg_value));
             }
-            IF_VERBOSE(0, verbose_stream() << "delay internalize @" << s().scope_lvl() << "\n");
+            IF_VERBOSE(2, verbose_stream() << "delay internalize @" << s().scope_lvl() << "\n");
             return false;
         }
         if (bv.is_zero(mul_value)) {