diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index d7ba4d604..073885c21 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -37,6 +37,7 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
     m_extract_prop = p.bv_extract_prop();
     m_ite2id = p.bv_ite2id();
     m_le_extra = p.bv_le_extra();
+    m_le2extract = p.bv_le2extract();
     set_sort_sums(p.bv_sort_ac());
 }
 
@@ -577,7 +578,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
             result = m().mk_eq(a, m_util.mk_numeral(numeral(0), bv_sz));
             return BR_REWRITE1;
         }
-        else if (first_non_zero < bv_sz - 1) {
+        else if (first_non_zero < bv_sz - 1 && m_le2extract) {
             result = m().mk_and(m().mk_eq(m_mk_extract(bv_sz - 1, first_non_zero + 1, a), m_util.mk_numeral(numeral(0), bv_sz - first_non_zero - 1)),
                                 m_util.mk_ule(m_mk_extract(first_non_zero, 0, a), m_mk_extract(first_non_zero, 0, b)));
             return BR_REWRITE3;
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 7b734dca1..7f0c67540 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -62,6 +62,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool       m_extract_prop;
     bool       m_bvnot_simpl;
     bool       m_le_extra;
+    bool       m_le2extract;
 
     bool is_zero_bit(expr * x, unsigned idx);
 
diff --git a/src/params/bv_rewriter_params.pyg b/src/params/bv_rewriter_params.pyg
index b439f2924..04c582485 100644
--- a/src/params/bv_rewriter_params.pyg
+++ b/src/params/bv_rewriter_params.pyg
@@ -11,5 +11,6 @@ def_module_params(module_name='rewriter',
                           ("bv_extract_prop", BOOL, False, "attempt to partially propagate extraction inwards"),
                           ("bv_not_simpl", BOOL, False, "apply simplifications for bvnot"),
                           ("bv_ite2id", BOOL, False, "rewrite ite that can be simplified to identity"),
-                          ("bv_le_extra", BOOL, False, "additional bu_(u/s)le simplifications")
+                          ("bv_le_extra", BOOL, False, "additional bu_(u/s)le simplifications"),
+                          ("bv_le2extract", BOOL, True, "disassemble bvule to extract")
                           ))