diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index 662358e91..c28a0a435 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -164,7 +164,7 @@ def mul {w : Nat} (x y : IntW w) (flags : NoWrapFlags := {nsw := false , nuw :=
   let umul := ux' * uy'
   let uhbound := shbound <<< 1
 
-  if flags.nsw ∧ (smul < slbound ∨ smul ≥ shbound) then
+  if flags.nsw ∧ ((smul <ₛ slbound) ∨ (smul ≥ₛ shbound)) then
     none
   else if flags.nuw ∧ umul ≥ uhbound then
     none
diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
index d4fdafa04..91a969e14 100644
--- a/SSA/Projects/InstCombine/TacticAuto.lean
+++ b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -226,6 +226,7 @@ macro "alive_auto": tactic =>
 macro "bv_compare'": tactic =>
   `(tactic|
       (
+        simp (config := {failIfUnchanged := false}) only [BitVec.twoPow] at *
         bv_compare
       )
    )