diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 516248e24..4740a954c 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -911,6 +911,11 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
         return BR_REWRITE2;
     }
 
+    if (arg1 == arg2) {
+        result = mk_numeral(0, bv_size);
+        return BR_DONE;
+    }
+
     return BR_FAILED;
 }
 
@@ -2250,10 +2255,10 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
     br_status st = mk_mul_core(num_args, args, result);
     if (st != BR_FAILED && st != BR_DONE)
         return st;
-    expr * x;
-    expr * y;
+    expr* x, * y, * z, * u;
     if (st == BR_FAILED && num_args == 2) {
-        x = args[0]; y = args[1];
+        x = args[0]; 
+        y = args[1];
     }
     else if (st == BR_DONE && is_mul(result) && to_app(result)->get_num_args() == 2) {
         x = to_app(result)->get_arg(0);
@@ -2262,7 +2267,25 @@ br_status bv_rewriter::mk_bv_mul(unsigned num_args, expr * const * args, expr_re
     else {
         return st;
     }
-
+    // ~x = -1 - x
+    unsigned sz = m_util.get_bv_size(x);
+    if (m_util.is_bv_not(x, z)) {
+        result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(-1, sz), z), y);
+        return BR_REWRITE3;
+    }
+    if (m_util.is_bv_not(y, z)) {
+        result = m_util.mk_bv_mul(m_util.mk_bv_sub(mk_numeral(-1, sz), z), x);
+        return BR_REWRITE3;
+    }
+    // shl(z, u) * x = shl(x * z, u)
+    if (m_util.is_bv_shl(x, z, u)) {
+        result = m_util.mk_bv_shl(m_util.mk_bv_mul(z, y), u);
+        return BR_REWRITE2;
+    }
+    if (m_util.is_bv_shl(y, z, u)) {
+        result = m_util.mk_bv_shl(m_util.mk_bv_mul(z, x), u);
+        return BR_REWRITE2;
+    }
     if (m_mul2concat) {
         numeral v;
         unsigned bv_size;