From 8ce2bb6df961aea048548608c0d277e4ca50e0af Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Mon, 13 May 2024 18:51:45 +0100
Subject: [PATCH] chore: disable unreachable tactic warning in AliveStatements
 (#302)

---
 SSA/Projects/InstCombine/AliveStatements.lean       | 2 ++
 SSA/Projects/InstCombine/update_alive_statements.py | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean
index 896b0011d..88782215e 100644
--- a/SSA/Projects/InstCombine/AliveStatements.lean
+++ b/SSA/Projects/InstCombine/AliveStatements.lean
@@ -12,6 +12,8 @@ import Mathlib.Data.BitVec.Lemmas
 open LLVM
 open BitVec
 
+set_option linter.unreachableTactic false
+
 
 theorem bitvec_AddSub_1043 :
     ∀ (e e_1 e_2 : LLVM.IntW w),
diff --git a/SSA/Projects/InstCombine/update_alive_statements.py b/SSA/Projects/InstCombine/update_alive_statements.py
index dda91b040..bc8f52154 100755
--- a/SSA/Projects/InstCombine/update_alive_statements.py
+++ b/SSA/Projects/InstCombine/update_alive_statements.py
@@ -21,6 +21,8 @@
 
 open LLVM
 open BitVec
+
+set_option linter.unreachableTactic false
 """