From 07116f9b9f8930212388d927a9063e55abf8719f Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Thu, 26 Jun 2025 16:57:37 +0100 Subject: [PATCH] feat: tweak simp_llvm_split simpset MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit While checking counter-examples, I noticed that some of the problems has a goal `value _ ⊑ poison`, which is impossible, so I added a rewrite to `False` to `simp_llvm_split`. --- SSA/Projects/InstCombine/Tactic/SimpLLVM.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/SSA/Projects/InstCombine/Tactic/SimpLLVM.lean b/SSA/Projects/InstCombine/Tactic/SimpLLVM.lean index ca0a662320..ea90514608 100644 --- a/SSA/Projects/InstCombine/Tactic/SimpLLVM.lean +++ b/SSA/Projects/InstCombine/Tactic/SimpLLVM.lean @@ -22,6 +22,8 @@ attribute [simp_llvm_split] if_if_eq_if_and if_if_eq_if_or PoisonOr.toOption_getSome PoisonOr.toOption_getSome PoisonOr.toOption_getNone + PoisonOr.not_value_isRefinedBy_poison + BitVec.ofBool_eq_one_iff /- `reduceOfInt` and `Nat.cast_one` are somewhat questionable additions to this simp-set. They are not needed for the case-bashing to succeed, but they are simp-lemmas that were previously being applied in `AliveAutoGenerated`, where they closed a few trivial goals,