diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index 5be9a1eea..090cd0e6c 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -310,7 +310,11 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
     SASSERT(!val(c).is_zero());
     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;        
+    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/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index 2f0c93fcf..8fb6725ce 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -480,6 +480,8 @@ namespace smt {
 #else
         strm << "lemma_" << (++m_lemma_id) << ".smt2";
 #endif
+        SASSERT(m_lemma_id != 341);
+        VERIFY(m_lemma_id != 341);
         return strm.str();
     }