From 69b4c9f43d53415748a88d9bbbe9576b6fa51173 Mon Sep 17 00:00:00 2001
From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
Date: Mon, 23 Sep 2024 11:44:24 +0100
Subject: [PATCH] chore: fixed `bv_auto` to prove `bv_AndOrXor_794` (#647)

---
 SSA/Projects/InstCombine/TacticAuto.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
index 8190e4fd3..8f4d34676 100644
--- a/SSA/Projects/InstCombine/TacticAuto.lean
+++ b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -112,7 +112,7 @@ macro "bv_auto": tactic =>
   `(tactic|
       (
         intros
-        try simp (config := {failIfUnchanged := false}) [(BitVec.negOne_eq_allOnes)]
+        try simp (config := {failIfUnchanged := false}) [-Bool.and_iff_left_iff_imp, (BitVec.negOne_eq_allOnes)]
         try ring_nf
         try bv_eliminate_bool
         repeat (split)
@@ -142,7 +142,6 @@ macro "bv_auto": tactic =>
             simp only [← BitVec.negOne_eq_allOnes]
             ring_nf
           | of_bool_tactic
-
           | (
               simp (config := {failIfUnchanged := false}) only [(BitVec.two_mul)]
               bv_automata