chore: fixed bv_auto to prove bv_AndOrXor_794 (#647)

opencompl · Sep 23, 2024 · 69b4c9f · 69b4c9f
1 parent 30d9e3c
commit 69b4c9f
Showing 1 changed file with 1 addition and 2 deletions.
diff --git 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