diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index f50dcebfa..e120f7baf 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -1446,18 +1446,34 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
 
 
 bool bv_rewriter::is_mul_no_overflow(expr* e) {
-    if (!m_util.is_bv_mul(e)) return false;
+    if (!m_util.is_bv_mul(e)) 
+        return false;
     unsigned sz = get_bv_size(e);
     unsigned sum = 0;
-    for (expr* x : *to_app(e)) sum += sz-num_leading_zero_bits(x);
-    return sum < sz;
+    for (expr* x : *to_app(e)) 
+        sum += sz - num_leading_zero_bits(x);
+    if (sum > sz + 1)
+        return false;
+    if (sum <= sz)
+        return true;
+    rational v;
+    unsigned shift;
+    for (expr* x : *to_app(e)) 
+        if (m_util.is_numeral(x, v) && v.is_power_of_two(shift))
+            return true;
+    return false;
 }
 
 bool bv_rewriter::is_add_no_overflow(expr* e) {
-    if (!is_add(e)) return false;
-    for (expr* x : *to_app(e)) {
-        if (0 == num_leading_zero_bits(x)) return false;
-    }
+    if (!is_add(e)) 
+        return false;
+    unsigned num_args = to_app(e)->get_num_args();
+    if (num_args <= 1)
+        return true;
+    num_args -= 2;
+    for (expr* x : *to_app(e)) 
+        if (num_args >= num_leading_zero_bits(x)) 
+            return false;
     return true;
 }