diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
index 6bf1e3b0c..2b2ab78c0 100644
--- a/SSA/Projects/InstCombine/TacticAuto.lean
+++ b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -189,6 +189,7 @@ macro "bv_ring" : tactic =>
       simp (config := {failIfUnchanged := false}) only [← BitVec.allOnes_sub_eq_xor,
         ← BitVec.negOne_eq_allOnes]
       ring_nf
+      rfl
       done
     )
    )
@@ -282,6 +283,7 @@ macro "bv_bench": tactic =>
       (
         all_goals (
           tac_bench [
+            "rfl" : (rfl; done),
             "bv_bitwise" : (bv_bitwise; done),
             "bv_ac" : (bv_ac; done),
             "bv_distrib" : (bv_distrib; done),