diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index badb35ae11..27fa7dd951 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -115,23 +115,79 @@ def alive_simplifyMulDivRem805 (w : Nat) :
   MulDivRem805_lhs w ⊑ MulDivRem805_rhs w := by
   unfold MulDivRem805_lhs MulDivRem805_rhs
   simp_alive_ssa
-  simp_alive_ops
-  simp_alive_undef
+  simp_llvm
   simp_alive_case_bash
-  simp only [ofInt_ofNat, add_eq, LLVM.icmp?_ult_eq, false_and, false_or, ite_false, PoisonOr.value_bind]
+  simp only [BitVec.one_sdiv]
+  simp only [ofNat_eq_ofNat, Bool.or_eq_true, beq_iff_eq, Bool.and_eq_true, bne_iff_ne, ne_eq,
+    ofBool_eq_one_iff, PoisonOr.ite_value_value, PoisonOr.if_then_poison_isRefinedBy_iff,
+    _root_.not_or, _root_.not_and, and_imp, PoisonOr.value_isRefinedBy_value,
+    InstCombine.bv_isRefinedBy_iff]
+  simp only [BitVec.ult, toNat_add, toNat_ofNat, Nat.mod_add_mod, decide_eq_true_eq]
+  intros x h₁ h₂
+  rcases w with _|_|w
+  · simp only [BitVec.eq_nil, not_true] at h₁
+  · match x with
+    | 1#1 => simp_all
+  · rw [Nat.mod_eq_of_lt (a := 3) (by
+      have := Nat.two_pow_pos w
+      simp [Nat.pow_succ];
+      omega)]
+
+    split
+    next h₁ =>
+      subst h₁
+      simp only [toNat_ofNat, lt_add_iff_pos_left, add_pos_iff, Nat.ofNat_pos, or_true,
+        Nat.one_mod_two_pow, Nat.reduceAdd, left_eq_ite_iff, not_lt, one_eq_zero_iff,
+        Nat.add_eq_zero, one_ne_zero, and_false, _root_.and_self, imp_false, not_le]
+      rw [Nat.mod_eq_of_lt]
+      · decide
+      · have := Nat.two_pow_pos w
+        simp [Nat.pow_succ]; omega
+    next h₁ =>
+      split
+      next h₂ =>
+        subst h₂
+        suffices (1 + (2 ^ (w + 1 + 1) - 1)) % 2 ^ (w + 1 + 1) < 3 by simpa
+        have := Nat.two_pow_pos w
+        rw [Nat.add_sub_of_le (by omega), Nat.mod_eq_of_lt]
+        · simp
+        · simp
+
+        calc
+          (1 + (2 ^ (w + 1 + 1) - 1)) % 2 ^ (w + 1 + 1)
+            = (2 ^ (w + 1 + 1)) % _ := by rw [Nat.add_sub_of_le]
+          _ = (2 ^ (w + 2)) % 2 ^ (w + 1 + 1) := by ac_rfl
+          _ < 3                               := sorry
+      next h₂ =>
+        simp
+
+
+    · simp_all
+    · rw [Nat.mod_eq_of_lt (by omega)] at *
+      contradiction
+    · simp_all
+    · simp_all
+    · simp_all
+
   cases w
   case zero =>
     intros x
-    simp only [BitVec.eq_nil]
-    simp [LLVM.sdiv?]
+    simp [BitVec.eq_nil x]
   case succ w' =>
     intros x
-    by_cases hx:(x = 0)
+    by_cases hx : x = 0#_
     case pos =>
       subst hx
-      rw [LLVM.sdiv?_denom_zero_eq_poison]
       simp
     case neg =>
+      simp [hx]
+      intro hx'
+      rw [BitVec.one_sdiv]
+      simp [BitVec.eq_ofNat_iff_toNat_eq]
+
+
+      stop
+
       rw [BitVec.ult_toNat]
       rw [BitVec.toNat_ofNat]
       cases w'
@@ -151,65 +207,45 @@ def alive_simplifyMulDivRem805 (w : Nat) :
       case succ w'' =>
         have htwopow_pos : 2^w'' > 0 := Nat.pow_pos (by omega)
         rw [Nat.mod_eq_of_lt (a := 3) (by omega)]
+        simp only [ofNat_eq_ofNat, Nat.reduceBneDiff, Bool.true_and, Bool.or_eq_true, beq_iff_eq,
+          Bool.and_eq_true, lt_add_iff_pos_left, add_pos_iff, Nat.ofNat_pos, or_true, msb_one,
+          Nat.add_eq_right, Nat.add_eq_zero, one_ne_zero, and_false, decide_false,
+          ne_intMin_of_lt_of_msb_false, false_and, or_false, toNat_add, toNat_ofNat,
+          Nat.one_mod_two_pow, ofBool_eq_one_iff, decide_eq_true_eq, PoisonOr.ite_value_value,
+          PoisonOr.if_then_poison_isRefinedBy_iff, PoisonOr.value_isRefinedBy_value,
+          InstCombine.bv_isRefinedBy_iff]
+        rintro h
+        rw [BitVec.one_sdiv]
+        split_ifs
+        · simp_all
+        · simp_all
+        · simp_all
+        · simp_all
+        · simp_all
+        · simp_all
+
+        stop
+
+        -- simp only [toNat_add, toNat_ofNat, Nat.mod_add_mod, Nat.reducePow, Fin.zero_eta,
+        --   Fin.isValue, ofFin_ofNat, ofNat_eq_ofNat, Option.some.injEq,
+        --   decide_eq_true_eq, eq_iff_iff, iff_false, not_lt] at hugt
         split
-        case isTrue hugt =>
-          have hugt :
-            (1 + BitVec.toNat x) % 2 ^ Nat.succ (Nat.succ w'') < 3 := by
-              by_contra hcontra
-              simp only [toNat_add, toNat_ofNat, Nat.mod_add_mod, hcontra, decide_false,
-                ofBool_false, ofNat_eq_ofNat, Nat.reducePow, Fin.mk_one, Fin.isValue, ofFin_ofNat,
-                Option.some.injEq] at hugt
-              contradiction
-          rw [LLVM.sdiv?_eq_value_of_neq_allOnes (hy := by tauto)]
-          · have hcases := Nat.cases_of_lt_mod_add hugt
-              (by simp)
-              (by apply BitVec.isLt)
-            rcases hcases with ⟨h1, h2⟩ | ⟨h1, h2⟩
-            · have h2 : BitVec.toNat x < 2 := by omega
-              have hneq0 : BitVec.toNat x ≠ 0 := BitVec.toNat_neq_zero_of_neq_zero hx
-              have h1 : BitVec.toNat x = 1 := by omega
-              have h1 : x = 1 := by
-                apply BitVec.eq_of_toNat_eq
-                simp only [h1, ofNat_eq_ofNat, toNat_ofNat]
-                rw [Nat.mod_eq_of_lt (by omega)]
-              subst h1
-              simp [BitVec.sdiv_one_one]
-            · have hcases : (1 + BitVec.toNat x = 2 ^ Nat.succ (Nat.succ w'') ∨
-                  1 + BitVec.toNat x = 2 ^ Nat.succ (Nat.succ w'') + 1) := by
-                omega
-              rcases hcases with heqallones | heqzero
-              · have heqallones : x = allOnes (Nat.succ (Nat.succ w'')) := by
-                  apply BitVec.eq_of_toNat_eq
-                  simp only [Nat.succ_eq_add_one, toNat_allOnes]
-                  omega
-                subst heqallones
-                simp [BitVec.sdiv_one_allOnes, BitVec.neg_one_eq_allOnes]
-              · have heqzero : x = 0#_ := BitVec.eq_zero_of_toNat_mod_eq_zero (by omega)
-                subst heqzero
-                simp [BitVec.sdiv_zero]
-          · exact intMin_neq_one (by omega)
-        case isFalse hugt =>
-          simp only [toNat_add, toNat_ofNat, Nat.mod_add_mod, Nat.reducePow, Fin.zero_eta,
-            Fin.isValue, ofFin_ofNat, ofNat_eq_ofNat, Option.some.injEq,
-            decide_eq_true_eq, eq_iff_iff, iff_false, not_lt] at hugt
-          unfold LLVM.sdiv? -- TODO: devar this; write theorem to unfold sdiv?
-          split <;> simp
-          case isFalse hsdiv =>
-            clear hsdiv
-            apply BitVec.one_sdiv (ha0 := by assumption)
-            · by_contra hone
-              subst hone
-              simp only [ofNat_eq_ofNat, toNat_ofNat,
-                Nat.add_mod_mod, Nat.reduceAdd] at hugt
-              rw [Nat.mod_eq_of_lt (a := 2) (by omega)] at hugt
-              contradiction
-            · by_contra hAllOnes
-              subst hAllOnes
-              rw [toNat_allOnes] at hugt
-              rw [Nat.add_sub_of_le (by omega)] at hugt
-              simp only [Nat.mod_self, Nat.ofNat_pos, decide_true,
-                ofBool_true, ofNat_eq_ofNat] at hugt
-              contradiction
+        case isFalse hsdiv =>
+          clear hsdiv
+          apply BitVec.one_sdiv (ha0 := by assumption)
+          · by_contra hone
+            subst hone
+            simp only [ofNat_eq_ofNat, toNat_ofNat,
+              Nat.add_mod_mod, Nat.reduceAdd] at hugt
+            rw [Nat.mod_eq_of_lt (a := 2) (by omega)] at hugt
+            contradiction
+          · by_contra hAllOnes
+            subst hAllOnes
+            rw [toNat_allOnes] at hugt
+            rw [Nat.add_sub_of_le (by omega)] at hugt
+            simp only [Nat.mod_self, Nat.ofNat_pos, decide_true,
+              ofBool_true, ofNat_eq_ofNat] at hugt
+            contradiction
 
 /--
 info: 'AliveHandwritten.MulDivRem.alive_simplifyMulDivRem805' depends on axioms: [propext, Classical.choice, Quot.sound]
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index f64b867482..8120e13680 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -207,31 +207,10 @@ lemma gt_one_of_neq_0_neq_1 (a : BitVec w) (ha0 : a ≠ 0) (ha1 : a ≠ 1) : a >
     have ha1' : a.toNat ≠ 1 := toNat_neq_of_neq_ofNat ha1
     omega
 
-def one_sdiv { w : Nat} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1)
+def one_sdiv_eq_zero { w : Nat} {a : BitVec w} (ha1 : a ≠ 1)
     (hao : a ≠ allOnes w) :
     BitVec.sdiv (1#w) a = 0#w := by
-  rcases w with ⟨rfl | ⟨rfl | w⟩⟩
-  case zero => simp [BitVec.eq_nil a]
-  case succ w' =>
-    cases w'
-    case zero =>
-      rcases eq_zero_or_eq_one a with ⟨rfl | rfl⟩ <;> (simp only [Nat.reduceAdd, ofNat_eq_ofNat, ne_eq,
-        not_true_eq_false] at ha0)
-      case inr h => subst h; contradiction
-    case succ w' =>
-      simp only [BitVec.sdiv, lt_add_iff_pos_left, add_pos_iff, zero_lt_one,
-        or_true, msb_one, neg_eq]
-      by_cases h : a.msb <;> simp [h]
-      · rw [← BitVec.udiv_eq, BitVec.udiv_eq_zero]
-        apply BitVec.gt_one_of_neq_0_neq_1
-        · rw [neg_ne_iff_ne_neg]
-          simp only [_root_.neg_zero]
-          assumption
-        · rw [neg_ne_iff_ne_neg]
-          rw [← neg_one_eq_allOnes] at hao
-          assumption
-      · rw [← BitVec.udiv_eq, BitVec.udiv_eq_zero]
-        apply BitVec.gt_one_of_neq_0_neq_1 <;> assumption
+  simp_all [one_sdiv, ← BitVec.neg_one_eq_allOnes]
 
 def sdiv_one_one : BitVec.sdiv 1#w 1#w = 1#w := by
   by_cases w_0 : w = 0; subst w_0; rfl
diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index 9a2dd40093..d1f2eac153 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -100,8 +100,68 @@ theorem Int.natCast_pred_of_pos (x : Nat) (h : 0 < x) :
       (-·), Int.neg, Int.negOfNat, Int.subNatNat]
     simp
 
+@[simp]
 theorem ofBool_eq_one_iff (b : Bool) :
     ofBool b = 1#1 ↔ b = true := by
   cases b <;> simp
 
+theorem one_udiv (x : BitVec w) :
+    (1#w) / x = if x = 1#w then 1#w else 0#w := by
+  rcases w with _|w
+  · simp
+  · apply eq_of_toNat_eq
+    have : x = 1#_ ↔ x.toNat = 1 := by
+      constructor
+      · rintro rfl; simp
+      · intro h; apply eq_of_toNat_eq; simp [h]
+    simp only [toNat_udiv, toNat_ofNat, Nat.zero_lt_succ, Nat.one_mod_two_pow, this]
+    match x.toNat with
+    | 0 | 1 | x + 2 => simp
+
+theorem one_sdiv (x : BitVec w) :
+    (1#w).sdiv x =
+      if x = 1#w then
+        1#w
+      else if x = -1#w then
+        -1#w
+      else
+        0#w := by
+  simp [BitVec.sdiv]
+  by_cases hw : w = 1
+  · subst hw
+    match x with
+    | 0#1 | 1#1 => rfl
+  · simp only [hw, decide_false]
+    by_cases hx : x = 1#w
+    · subst hx
+      simp [hw]
+    by_cases hx : x = -1#w
+    · subst hx
+      have : w ≠ 0 := by rintro rfl; contradiction
+      have : (1#w != 0#w) = true := by simp [*]
+      have : (1#w != intMin _) = true := by
+        simp only [bne_iff_ne, ne_eq, intMin]
+        intro contra
+        have : (twoPow w (w - 1)).toNat = 1 := by
+          simp [← contra]; omega
+        obtain ⟨_, rfl⟩ := Nat.exists_eq_add_of_lt (by omega : 1 < w)
+        rw [toNat_twoPow, Nat.mod_eq_of_lt] at this
+        · simp at this
+        · simp; omega
+      simp [*, BitVec.msb_neg]
+    · simp [*]
+      cases hx : x.msb
+      · simp [one_udiv, *]
+      · simp [one_udiv, *]
+        intro h_neg_x
+        exfalso
+        apply ‹x ≠ -1#w›
+        rw [← BitVec.neg_neg (x := x), h_neg_x]
+
+theorem eq_ofNat_iff_toNat_eq (x : BitVec w) (n : Nat) :
+    x = BitVec.ofNat w n ↔ x.toNat = n % 2 ^ w := by
+  constructor
+  · rintro rfl; simp
+  · intro h; apply BitVec.eq_of_toNat_eq; simpa
+
 end BitVec
diff --git a/SSA/Projects/InstCombine/LLVM/Semantics.lean b/SSA/Projects/InstCombine/LLVM/Semantics.lean
index c97a4774a3..80e4ed243f 100644
--- a/SSA/Projects/InstCombine/LLVM/Semantics.lean
+++ b/SSA/Projects/InstCombine/LLVM/Semantics.lean
@@ -54,41 +54,27 @@ end IntW
 The ‘and’ instruction returns the bitwise logical and of its two operands.
 -/
 @[simp_llvm]
-def and? {w : Nat} (x y : BitVec w) : IntW w :=
-  .value <| x &&& y
-
-@[simp_llvm_option]
-theorem and?_eq : LLVM.and? a b  = .value (a &&& b) := rfl
-
-@[simp_llvm_option]
 def and {w : Nat} (x y : IntW w) : IntW w := do
   let x' ← x
   let y' ← y
-  and? x' y'
+  .value <| x' &&& y'
+
+structure DisjointFlag where
+  disjoint : Bool := false
+  deriving Repr, DecidableEq, Lean.ToExpr
 
 /--
 The ‘or’ instruction returns the bitwise logical inclusive or of its two
 operands.
 -/
 @[simp_llvm]
-def or? {w : Nat} (x y : BitVec w) : IntW w :=
-  .value <| x ||| y
-
-@[simp_llvm_option]
-theorem or?_eq : LLVM.or? a b  = .value (a ||| b) := rfl
-
-structure DisjointFlag where
-  disjoint : Bool := false
-  deriving Repr, DecidableEq, Lean.ToExpr
-
-@[simp_llvm_option]
 def or {w : Nat} (x y : IntW w)  (flag : DisjointFlag := {disjoint := false}) : IntW w := do
   let x' ← x
   let y' ← y
   if flag.disjoint ∧ x' &&& y' != 0 then
     .poison
   else
-    or? x' y'
+    .value <| x' ||| y'
 
 /--
 The ‘xor’ instruction returns the bitwise logical exclusive or of its two
@@ -96,17 +82,15 @@ operands.  The xor is used to implement the “one’s complement” operation,
 is the “~” operator in C.
 -/
 @[simp_llvm]
-def xor? {w : Nat} (x y : BitVec w) : IntW w :=
-  .value <| x ^^^ y
-
-@[simp_llvm_option]
-theorem xor?_eq : LLVM.xor? a b  = .value (a ^^^ b) := rfl
-
-@[simp_llvm_option]
 def xor {w : Nat} (x y : IntW w) : IntW w := do
   let x' ← x
   let y' ← y
-  xor? x' y'
+  .value <| x' ^^^ y'
+
+structure NoWrapFlags where
+  nsw : Bool := false
+  nuw : Bool := false
+  deriving Repr, DecidableEq, Lean.ToExpr
 
 /--
 The value produced is the integer sum of the two operands.
@@ -114,18 +98,6 @@ If the sum has unsigned overflow, the result returned is the mathematical result
 Because LLVM integers use a two’s complement representation, this instruction is appropriate for both signed and unsigned integers.
 -/
 @[simp_llvm]
-def add? {w : Nat} (x y : BitVec w) : IntW w :=
-  .value <| x + y
-
-@[simp_llvm_option]
-theorem add?_eq : LLVM.add? a b  = .value (a + b) := rfl
-
-structure NoWrapFlags where
-  nsw : Bool := false
-  nuw : Bool := false
-  deriving Repr, DecidableEq, Lean.ToExpr
-
-@[simp_llvm_option]
 def add {w : Nat} (x y : IntW w) (flags : NoWrapFlags := {nsw := false , nuw := false}) : IntW w := do
   let x' ← x
   let y' ← y
@@ -134,7 +106,7 @@ def add {w : Nat} (x y : IntW w) (flags : NoWrapFlags := {nsw := false , nuw :=
   else if flags.nuw ∧ BitVec.uaddOverflow x' y' then
     .poison
   else
-    add? x' y'
+    .value <| x' + y'
 
 /--
 The value produced is the integer difference of the two operands.
@@ -142,13 +114,6 @@ If the difference has unsigned overflow, the result returned is the mathematical
 Because LLVM integers use a two’s complement representation, this instruction is appropriate for both signed and unsigned integers.
 -/
 @[simp_llvm]
-def sub? {w : Nat} (x y : BitVec w) : IntW w :=
-  .value <| x - y
-
-@[simp_llvm_option]
-theorem sub?_eq : LLVM.sub? a b  = .value (a - b) := rfl
-
-@[simp_llvm_option]
 def sub {w : Nat} (x y : IntW w) (flags : NoWrapFlags := {nsw := false , nuw := false}) : IntW w := do
   let x' ← x
   let y' ← y
@@ -157,7 +122,7 @@ def sub {w : Nat} (x y : IntW w) (flags : NoWrapFlags := {nsw := false , nuw :=
   else if flags.nuw ∧ BitVec.usubOverflow x' y' then
     .poison
   else
-    sub? x' y'
+    .value <| x' - y'
 
 /--
 The value produced is the integer product of the two operands.
@@ -171,13 +136,6 @@ If a full product (e.g. i32 * i32 -> i64) is needed, the operands should be
 sign-extended or zero-extended as appropriate to the width of the full product.
 -/
 @[simp_llvm]
-def mul? {w : Nat} (x y : BitVec w) : IntW w :=
-  .value <| x * y
-
-@[simp_llvm_option]
-theorem mul?_eq : LLVM.mul? a b  = .value (a * b) := rfl
-
-@[simp_llvm_option]
 def mul {w : Nat} (x y : IntW w) (flags : NoWrapFlags := {nsw := false , nuw := false}) : IntW w := do
   let x' ← x
   let y' ← y
@@ -187,7 +145,11 @@ def mul {w : Nat} (x y : IntW w) (flags : NoWrapFlags := {nsw := false , nuw :=
   else if flags.nuw ∧ BitVec.umulOverflow x' y' then
     .poison
   else
-    mul? x' y'
+    .value <| x' * y'
+
+structure ExactFlag where
+  exact : Bool := false
+  deriving Repr, DecidableEq, Lean.ToExpr
 
 /--
 The value produced is the unsigned integer quotient of the two operands.
@@ -195,24 +157,15 @@ Note that unsigned integer division and signed integer division are distinct ope
 Division by zero is undefined behavior.
 -/
 @[simp_llvm]
-def udiv? {w : Nat} (x y : BitVec w) : IntW w :=
-  if y = 0 then
-    .poison
-  else
-    .value <| x / y
-
-structure ExactFlag where
-  exact : Bool := false
-  deriving Repr, DecidableEq, Lean.ToExpr
-
-@[simp_llvm_option]
 def udiv {w : Nat} (x y : IntW w) (flag : ExactFlag := {exact := false}) : IntW w := do
   let x' ← x
   let y' ← y
   if flag.exact ∧ x'.umod y' ≠ 0 then
     .poison
+  else if y' = 0 then
+    .poison
   else
-    udiv? x' y'
+    .value <| x' / y'
 
 /--
 The value produced is the signed integer quotient of the two operands rounded towards zero.
@@ -247,7 +200,7 @@ theorem sdiv?_eq_value_of_neq_allOnes {x y : BitVec w} (hy : y ≠ 0)
   simp [LLVM.sdiv?]
   tauto
 
-@[simp_llvm_option]
+@[simp_llvm]
 def sdiv {w : Nat} (x y : IntW w) (flag : ExactFlag := {exact := false}) : IntW w := do
   let x' ← x
   let y' ← y
@@ -272,17 +225,13 @@ Note that unsigned integer remainder and signed integer remainder are distinct o
 Taking the remainder of a division by zero is undefined behavior.
 -/
 @[simp_llvm]
-def urem? {w : Nat} (x y : BitVec w) : IntW w :=
-  if y = 0 then
-    .poison
-  else
-    .value <| x % y
-
-@[simp_llvm_option]
 def urem {w : Nat} (x y : IntW w) : IntW w := do
   let x' ← x
   let y' ← y
-  urem? x' y'
+  if y' = 0 then
+    .poison
+  else
+    .value <| x' % y'
 
 @[simp_llvm]
 def _root_.Int.rem (x y : Int) : Int :=
@@ -340,7 +289,7 @@ def srem? {w : Nat} (x y : BitVec w) : IntW w :=
   else
     .value <| BitVec.srem x y
 
-@[simp_llvm_option]
+@[simp_llvm]
 def srem {w : Nat} (x y : IntW w) : IntW w := do
   let x' ← x
   let y' ← y
@@ -362,7 +311,7 @@ def shl? {n} (op1 : BitVec n) (op2 : BitVec n) : IntW n :=
   else .value (op1 <<< op2)
 
 
-@[simp_llvm_option]
+@[simp_llvm]
 def shl {w : Nat} (x y : IntW w) (flags : NoWrapFlags := {nsw := false , nuw := false}) : IntW w := do
   let x' ← x
   let y' ← y
@@ -390,7 +339,7 @@ def lshr? {n} (op1 : BitVec n) (op2 : BitVec n) : IntW n :=
   then .poison
   else .value (op1 >>> op2)
 
-@[simp_llvm_option]
+@[simp_llvm]
 def lshr {w : Nat} (x y : IntW w) (flag : ExactFlag := {exact := false}) : IntW w := do
   let x' ← x
   let y' ← y
@@ -414,7 +363,7 @@ def ashr? {n} (op1 : BitVec n) (op2 : BitVec n) : IntW n :=
   then .poison
   else .value (op1.sshiftRight' op2)
 
-@[simp_llvm_option]
+@[simp_llvm]
 def ashr {w : Nat} (x y : IntW w) (flag : ExactFlag := {exact := false}) : IntW w := do
   let x' ← x
   let y' ← y
@@ -426,7 +375,7 @@ def ashr {w : Nat} (x y : IntW w) (flag : ExactFlag := {exact := false}) : IntW
 /--
  If the condition is an i1 and it evaluates to 1, the instruction returns the first value argument; otherwise, it returns the second value argument.
 -/
-@[simp_llvm_option]
+@[simp_llvm]
 def select {w : Nat} (c? : IntW 1) (x? y? : IntW w ) : IntW w := do
   let c ← c?
   if c = 1#1 then x? else y?
@@ -527,7 +476,7 @@ theorem icmp?_slt_eq {w : Nat} {a b : BitVec w} :
 theorem icmp?_sgt_eq {w : Nat} {a b : BitVec w} :
   icmp? .sgt a b = .value (BitVec.ofBool (a >ₛ b)) := rfl
 
-@[simp_llvm_option]
+@[simp_llvm]
 def icmp {w : Nat} (c : IntPred) (x y : IntW w) : IntW 1 := do
   let x' ← x
   let y' ← y
@@ -554,17 +503,17 @@ TODO: double-check that truncating works the same as MLIR (signedness, overflow,
 def const? (w : Nat) (i : Int): IntW w :=
   .value <| BitVec.ofInt w i
 
-@[simp_llvm_option]
+@[simp_llvm]
 theorem const?_eq : LLVM.const? w i = .value (BitVec.ofInt w i) := rfl
 
 @[simp_llvm]
 def not? {w : Nat} (x : BitVec w) : IntW w := do
   .value (~~~x)
 
-@[simp_llvm_option]
+@[simp_llvm]
 theorem not?_eq : LLVM.not? a = .value (~~~ a) := rfl
 
-@[simp_llvm_option]
+@[simp_llvm]
 def not {w : Nat} (x : IntW w) : IntW w := do
   let x' ← x
   not? x'
@@ -573,10 +522,10 @@ def not {w : Nat} (x : IntW w) : IntW w := do
 def neg? {w : Nat} (x : BitVec w) : IntW w := do
   .value <| (-.) x
 
-@[simp_llvm_option]
+@[simp_llvm]
 theorem neg?_eq : LLVM.neg? a = .value (-a) := rfl
 
-@[simp_llvm_option]
+@[simp_llvm]
 def neg {w : Nat} (x : IntW w) : IntW w := do
   let x' ← x
   neg? x'
@@ -586,7 +535,7 @@ def neg {w : Nat} (x : IntW w) : IntW w := do
 def trunc? {w: Nat} (w': Nat) (x: BitVec w) : IntW w' := do
   .value <| (BitVec.truncate w' x)
 
-@[simp_llvm_option]
+@[simp_llvm]
 def trunc {w: Nat} (w': Nat) (x: IntW w) (noWrapFlags : NoWrapFlags := {nsw := false , nuw := false}) : IntW w' := do
   let x' <- x
   if noWrapFlags.nsw ∧ ((x'.truncate w').signExtend w ≠ x') then
@@ -604,7 +553,7 @@ structure NonNegFlag where
 def zext? {w: Nat} (w': Nat) (x: BitVec w) : IntW w' := do
   .value <| (BitVec.zeroExtend w' x)
 
-@[simp_llvm_option]
+@[simp_llvm]
 def zext {w: Nat} (w': Nat) (x: IntW w) (flag : NonNegFlag := {nneg := false}) : IntW w' := do
   let x' <- x
   if flag.nneg ∧ x'.msb then
@@ -616,7 +565,7 @@ def zext {w: Nat} (w': Nat) (x: IntW w) (flag : NonNegFlag := {nneg := false}) :
 def sext? {w: Nat} (w': Nat) (x: BitVec w) : IntW w' := do
   .value <| (BitVec.signExtend w' x)
 
-@[simp_llvm_option]
+@[simp_llvm]
 def sext {w: Nat} (w': Nat) (x: IntW w) : IntW w' := do
   let x' <- x
   sext? w' x'
diff --git a/SSA/Projects/InstCombine/LLVM/SimpSet.lean b/SSA/Projects/InstCombine/LLVM/SimpSet.lean
index 1c0e367fe8..301a86331b 100644
--- a/SSA/Projects/InstCombine/LLVM/SimpSet.lean
+++ b/SSA/Projects/InstCombine/LLVM/SimpSet.lean
@@ -6,7 +6,6 @@ import Lean.Meta.Tactic.Simp.RegisterCommand
 import Lean.LabelAttribute
 
 register_simp_attr simp_llvm
-register_simp_attr simp_llvm_option
 
 /-- The simp-set used in `simp_alive_case_bash` to attempt to discharge trivial `none` cases -/
 register_simp_attr simp_llvm_case_bash
diff --git a/SSA/Projects/InstCombine/Tactic/SimpLLVM.lean b/SSA/Projects/InstCombine/Tactic/SimpLLVM.lean
index 98fd305507..93ce86f8b5 100644
--- a/SSA/Projects/InstCombine/Tactic/SimpLLVM.lean
+++ b/SSA/Projects/InstCombine/Tactic/SimpLLVM.lean
@@ -23,12 +23,12 @@ attribute [simp_llvm_split]
    previously being applied in `AliveAutoGenerated`, where they closed a few trivial goals,
    so they've been preserved to not change this existing behaviour of `simp_alive_case_bash` -/
 
-attribute [simp_llvm_option]
+attribute [simp_llvm]
   PoisonOr.value_bind PoisonOr.isRefinedBy_poison_iff
   PoisonOr.value_ne_poison PoisonOr.poison_ne_value
 
 open PoisonOr in
-@[simp_llvm_option]
+@[simp_llvm]
 theorem LLVM.IntW.value_isRefinedBy_iff (a : BitVec w) (b? : PoisonOr (BitVec w)) :
     value a ⊑ b? ↔ b? = value a := by
   cases b? <;> (
@@ -99,31 +99,27 @@ macro_rules
     )
   )
 
+/-! ## `simp_llvm` -/
 
-/-- Unfold into the `undef' statements and eliminates as much as possible. -/
-macro "simp_alive_undef" : tactic =>
-  `(tactic|
-      (
-        simp (config := {failIfUnchanged := false}) only [
-            simp_llvm_option,
-            bind_assoc,
-            Bool.false_eq_true, false_and, reduceIte,
-            (BitVec.ofInt_ofNat)
-          ]
-      )
-  )
+/--
+`simp_llvm` unfolds LLVM semantics functions into monadic bitvector expressions,
+simplifying trivial refinements in the process.
+-/
+macro "simp_llvm" : tactic => `(tactic|(
+  simp (config := {failIfUnchanged := false}) only [
+    simp_llvm,
+    (BitVec.ofInt_ofNat)]
+))
 
 attribute [simp_llvm]
+  bind_assoc
+  Bool.false_eq_true false_and reduceIte
   pure_bind
   BitVec.ofInt_neg_one
   PoisonOr.bind_if_then_poison_eq_ite_bind
   PoisonOr.bind_if_else_poison_eq_ite_bind
 
-/- Simplify away the `InstCombine` specific semantics. -/
-macro "simp_alive_ops" : tactic =>
-  `(tactic|(
-      simp (config := {failIfUnchanged := false}) only [
-          simp_llvm,
-          (BitVec.ofInt_ofNat)
-        ]
-    ))
+@[deprecated "use `simp_llvm` instead" (since := "2025-05-12")]
+macro "simp_alive_ops" : tactic => `(tactic| simp_llvm)
+@[deprecated "use `simp_llvm` instead" (since := "2025-05-12")]
+macro "simp_alive_undef" : tactic => `(tactic| simp_llvm)
diff --git a/SSA/Projects/SLLVM/Tactic.lean b/SSA/Projects/SLLVM/Tactic.lean
index ecdffce845..01b0f957cc 100644
--- a/SSA/Projects/SLLVM/Tactic.lean
+++ b/SSA/Projects/SLLVM/Tactic.lean
@@ -4,7 +4,7 @@ import SSA.Projects.InstCombine.Tactic.SimpLLVM
 import SSA.Projects.SLLVM.Tactic.SimpSet
 
 macro "simp_sllvm" : tactic => `(tactic|(
-  simp -failIfUnchanged only [simp_sllvm, simp_llvm, simp_llvm_option]
+  simp -failIfUnchanged only [simp_sllvm, simp_llvm, simp_llvm]
 ))
 
 attribute [simp_sllvm]