diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
index 73787ed8d..1b38a2878 100644
--- a/SSA/Projects/InstCombine/TacticAuto.lean
+++ b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -91,6 +91,15 @@ macro "simp_alive_bitvec": tactic =>
                      try cases BitVec.getLsb _ _ <;> try simp;
                      try cases BitVec.getLsb _ _ <;> try simp;)
         try solve | (simp [bv_ofBool])
+        /-
+        There are 2 main kinds of operations on BitVecs
+        1. Boolean operations (^^^, &&&, |||) which can be solved by extensionality.
+        2. Arithmetic operations (+, -) which can be solved by `ring_nf`.
+        The purpose of the below line is to convert boolean
+        operations to arithmetic operations and then
+        solve the arithmetic with the `ring_nf` tactic.
+        -/
+        try solve | (simp only [← BitVec.allOnes_sub_eq_xor, BitVec.negOne_eq_allOnes']; ring_nf)
       )
    )