doc: remarks about multiplication (#5636)

leanprover · Oct 7, 2024 · 99a9d9b · 99a9d9b
1 parent 1914a2b
commit 99a9d9b
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
@@ -15,8 +15,9 @@ circuit mirrors the behavior of `BitVec.mulRec`.
 
 Note that the implementation performs a symbolic branch over the bits of the right hand side.
 Thus if the right hand side is (partially) known through constant propagation etc. the symbolic
-branches will be (partially) constant folded away by the AIG optimizer. The preprocessing simp set
-of `bv_decide` ensures that constants always end up on the right hand side for this reason.
+branches will be (partially) constant folded away by the AIG optimizer. The preprocessing of
+`blastMul` ensures that the value with more known bits always end up on the right hand side for
+this reason.
 -/
 
 namespace Std.Tactic.BVDecide

diff --git a/tests/lean/run/bv_arith.lean b/tests/lean/run/bv_arith.lean
@@ -22,7 +22,7 @@ theorem arith_unit_3 (x y : BitVec 16) : x - (x - y) = y := by
 theorem arith_unit_4 (x y : BitVec 4) : x * y = y * x := by
   bv_decide
 
-theorem arith_unit_5 (x : BitVec 8) : x * 32 = 32 * x := by
+theorem arith_unit_5 (x : BitVec 64) : x * 32 = 32 * x := by
   bv_decide
 
 theorem arith_unit_6 (x : BitVec 64) : x + x = 2 * x := by