diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index edd601c9c..75f931c1d 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -1365,13 +1365,88 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
         result = m_autil.mk_numeral(v, true);
         return BR_DONE;
     }
-
-    // TODO: add other simplifications
+    if (m_util.is_concat(arg)) {
+        if (to_app(arg)->get_num_args() == 0) {
+            result = m_autil.mk_int(0);
+            return BR_DONE;
+        }
+        expr_ref_vector args(m());        
+        
+        unsigned num_args = to_app(arg)->get_num_args();
+        for (expr* x : *to_app(arg)) {
+            args.push_back(m_util.mk_bv2int(x));
+        }
+        unsigned sz = get_bv_size(to_app(arg)->get_arg(num_args-1));
+        for (unsigned i = num_args - 1; i > 0; ) {
+            expr_ref tmp(m());
+            --i;
+            tmp = args[i].get();
+            tmp = m_autil.mk_mul(m_autil.mk_numeral(power(numeral(2), sz), true), tmp);
+            args[i] = tmp;
+            sz += get_bv_size(to_app(arg)->get_arg(i));
+        }
+        result = m_autil.mk_add(args.size(), args.c_ptr());
+        return BR_REWRITE2;
+    }
+    if (is_mul_no_overflow(arg)) {
+        expr_ref_vector args(m());
+        for (expr* x : *to_app(arg)) args.push_back(m_util.mk_bv2int(x));
+        result = m_autil.mk_mul(args.size(), args.c_ptr());
+        return BR_REWRITE2;
+    }
+    if (is_add_no_overflow(arg)) {
+        expr_ref_vector args(m());
+        for (expr* x : *to_app(arg)) args.push_back(m_util.mk_bv2int(x));
+        result = m_autil.mk_add(args.size(), args.c_ptr());
+        return BR_REWRITE2;
+    }
 
     return BR_FAILED;
 }
 
 
+bool bv_rewriter::is_mul_no_overflow(expr* e) {
+    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;
+}
+
+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;
+    }
+    return true;
+}
+
+unsigned bv_rewriter::num_leading_zero_bits(expr* e) {
+    numeral v;
+    unsigned sz = get_bv_size(e);
+    if (m_util.is_numeral(e, v)) {
+        while (v.is_pos()) {
+            SASSERT(sz > 0);
+            --sz;
+            v = div(v, numeral(2));
+        }
+        return sz;
+    }
+    else if (m_util.is_concat(e)) {
+        app* a = to_app(e);
+        unsigned sz1 = get_bv_size(a->get_arg(0));
+        unsigned nb1 = num_leading_zero_bits(a->get_arg(0));
+        if (sz1 == nb1) {
+            nb1 += num_leading_zero_bits(a->get_arg(1));
+        }
+        return nb1;
+    }
+    return 0;
+}
+
+
+
+
 br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_ref & result) {
     expr_ref_buffer new_args(m());
     numeral v1;
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 45bd6c264..205ebbf8e 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -42,6 +42,7 @@ protected:
     decl_kind mul_decl_kind() const { return OP_BMUL; }
     bool use_power() const { return false; }
     decl_kind power_decl_kind() const { UNREACHABLE(); return static_cast<decl_kind>(UINT_MAX); }
+
 public:
     bv_rewriter_core(ast_manager & m):m_util(m) {}
 };
@@ -108,6 +109,10 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     br_status mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result);
     bool is_minus_one_core(expr * arg) const;
     bool is_x_minus_one(expr * arg, expr * & x);
+    bool is_add_no_overflow(expr* e);
+    bool is_mul_no_overflow(expr* e);
+    unsigned num_leading_zero_bits(expr* e);
+
     br_status mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);
     br_status mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);
     br_status mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);