diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index f8ff27337..44efe0199 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -63,6 +63,7 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
     m_blast_eq_value = p.blast_eq_value();
     m_split_concat_eq = p.split_concat_eq();
     m_udiv2mul = p.udiv2mul();
+    m_bvnot2arith = p.bvnot2arith();
     m_mkbv2num = _p.get_bool("mkbv2num", false);
 }
 
@@ -1527,6 +1528,14 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
     }
 #endif
 
+    if (m_bvnot2arith) {
+        // (bvnot x) --> (bvsub -1 x)
+        bv_size = get_bv_size(arg);
+        rational minus_one = (rational::power_of_two(bv_size) - numeral(1));
+        result = m_util.mk_bv_sub(m_util.mk_numeral(minus_one, bv_size), arg);
+        return BR_REWRITE1;
+    }
+
     return BR_FAILED;
 }
 
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index ba5ac5580..a94fd18c1 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -67,6 +67,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool       m_mkbv2num;
     bool       m_split_concat_eq;
     bool       m_udiv2mul;
+    bool       m_bvnot2arith;
 
     bool is_zero_bit(expr * x, unsigned idx);
 
diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg
index 780d8e724..d9ee9f7a3 100644
--- a/src/ast/rewriter/bv_rewriter_params.pyg
+++ b/src/ast/rewriter/bv_rewriter_params.pyg
@@ -7,4 +7,6 @@ def_module_params(module_name='rewriter',
                           ("blast_eq_value", BOOL, False, "blast (some) Bit-vector equalities into bits"),
                           ("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"),
                           ("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
-                          ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation")))
+                          ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
+                          ("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)")
+                          ))