diff --git a/src/Lean/Elab/Tactic/BVDecide/External.lean b/src/Lean/Elab/Tactic/BVDecide/External.lean
index 6f498afc86..2b58e2de4f 100644
--- a/src/Lean/Elab/Tactic/BVDecide/External.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/External.lean
@@ -169,8 +169,9 @@ def satQuery (solverPath : System.FilePath) (problemPath : System.FilePath) (pro
   let out? ← runInterruptible timeout { cmd, args, stdin := .piped, stdout := .piped, stderr := .null }
   match out? with
   | .timeout =>
-    let mut err := "The SAT solver timed out while solving the problem."
-    err := err ++ "\nConsider increasing the timeout with `set_option sat.timeout <sec>`"
+    let mut err := "The SAT solver timed out while solving the problem.\n"
+    err := err ++ "Consider increasing the timeout with `set_option sat.timeout <sec>`.\n"
+    err := err ++ "If solving your problem relies inherently on using associativity or commutativity, consider enabling the `bv.ac_nf` option."
     throwError err
   | .success { exitCode := exitCode, stdout := stdout, stderr := stderr} =>
     if exitCode == 255 then
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean
index d5139298be..ce770dd5d5 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Attr.lean
@@ -53,7 +53,7 @@ register_builtin_option debug.bv.graphviz : Bool := {
 }
 
 register_builtin_option bv.ac_nf : Bool := {
-  defValue := true
+  defValue := false
   descr := "Canonicalize with respect to associativity and commutativitiy."
 }
 
diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean
index 68c4a6a6c5..aeedb45f04 100644
--- a/src/Std/Tactic/BVDecide/Syntax.lean
+++ b/src/Std/Tactic/BVDecide/Syntax.lean
@@ -46,6 +46,10 @@ terms that were considered as variables.
 
 In order to avoid calling a SAT solver every time, the proof can be cached with `bv_decide?`.
 
+If solving your problem relies inherently on using associativity or commutativity, consider enabling
+the `bv.ac_nf` option.
+
+
 Note: `bv_decide` uses `ofReduceBool` and thus trusts the correctness of the code generator.
 -/
 syntax (name := bvDecide) "bv_decide" : tactic
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 81cf3a1e34..0d4c7c2a07 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -17,12 +17,6 @@ example :
 example (x y z : BitVec 8) (h1 : x = z → False) (h2 : x = y) (h3 : y = z) : False := by
   bv_decide
 
-example (x y : BitVec 256) : x * y = y * x := by
-  bv_decide
-
-example {x y z : BitVec 64} : ~~~(x &&& (y * z)) = (~~~x ||| ~~~(z * y)) := by
-  bv_decide
-
 def mem_subset (a1 a2 b1 b2 : BitVec 64) : Bool :=
   (b2 - b1 = BitVec.ofNat 64 (2^64 - 1)) ||
   ((a2 - b1 <= b2 - b1 && a1 - b1 <= a2 - b1))
@@ -84,3 +78,18 @@ example {x : BitVec 16} : (10 + x) + 2 = 12 + x := by bv_normalize
 example {x : BitVec 16} : (x + 10) + 2 = 12 + x := by bv_normalize
 example {x : BitVec 16} : 2 + (x + 10) = 12 + x := by bv_normalize
 example {x : BitVec 16} : 2 + (10 + x) = 12 + x := by bv_normalize
+
+
+
+
+section
+
+set_option bv.ac_nf true
+
+example (x y : BitVec 256) : x * y = y * x := by
+  bv_decide
+
+example {x y z : BitVec 64} : ~~~(x &&& (y * z)) = (~~~x ||| ~~~(z * y)) := by
+  bv_decide
+
+end
diff --git a/tests/lean/run/bv_errors.lean b/tests/lean/run/bv_errors.lean
index caa39cb26f..29023911f9 100644
--- a/tests/lean/run/bv_errors.lean
+++ b/tests/lean/run/bv_errors.lean
@@ -6,7 +6,8 @@ set_option bv.ac_nf false
 
 /--
 error: The SAT solver timed out while solving the problem.
-Consider increasing the timeout with `set_option sat.timeout <sec>`
+Consider increasing the timeout with `set_option sat.timeout <sec>`.
+If solving your problem relies inherently on using associativity or commutativity, consider enabling the `bv.ac_nf` option.
 -/
 #guard_msgs in
 set_option sat.timeout 1 in