diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index be8464c70..8895ac855 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -1336,6 +1336,10 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
             result = mk_numeral(0, bv_size);
             return BR_REWRITE2;
         }
+
+        if (r2.is_pos()) {
+            
+        }
     }
 
     if (hi_div0) {
diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp
index d46e2db07..717091f53 100644
--- a/src/math/lp/nla_monotone_lemmas.cpp
+++ b/src/math/lp/nla_monotone_lemmas.cpp
@@ -53,6 +53,8 @@ void monotone::monotonicity_lemma_gt(const monic& m) {
     for (lpvar j : m.vars()) {
         auto v = c().val(j);
         lemma |= ineq(j, v.is_neg() ? llc::LT : llc::GT, v);
+        if (v.is_neg())
+            lemma |= ineq(j, llc::GT, 0);
         product *= v;
     }
     lemma |= ineq(m.var(), product.is_neg() ? llc::GE : llc::LE, product);