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,