diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 9f35e7b4a381..5158f466416a 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2115,6 +2115,8 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
 
 /-! ### abs -/
 
+theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
+
 @[simp, bv_toNat]
 theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
   simp only [BitVec.abs, neg_eq]
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index 13af0cd31e81..bf4e4680bc1b 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -29,7 +29,6 @@ instance : ToExpr BVBinOp where
     | .mul => mkConst ``BVBinOp.mul
     | .udiv => mkConst ``BVBinOp.udiv
     | .umod => mkConst ``BVBinOp.umod
-    | .sdiv => mkConst ``BVBinOp.sdiv
   toTypeExpr := mkConst ``BVBinOp
 
 instance : ToExpr BVUnOp where
@@ -103,6 +102,7 @@ where
   | .const b => mkApp2 (mkConst ``BoolExpr.const) (toTypeExpr α) (toExpr b)
   | .not x => mkApp2 (mkConst ``BoolExpr.not) (toTypeExpr α) (go x)
   | .gate g x y => mkApp4 (mkConst ``BoolExpr.gate) (toTypeExpr α) (toExpr g) (go x) (go y)
+  | .ite d l r => mkApp4 (mkConst ``BoolExpr.ite) (toTypeExpr α) (go d) (go l) (go r)
 
 
 open Lean.Meta
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
index da62556ac44d..b0c1335284fa 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean
@@ -57,7 +57,8 @@ Construct the reified version of applying the gate in `gate` to `lhs` and `rhs`.
 This function assumes that `lhsExpr` and `rhsExpr` are the corresponding expressions to `lhs`
 and `rhs`.
 -/
-def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) : M ReifiedBVLogical := do
+def mkGate (lhs rhs : ReifiedBVLogical) (lhsExpr rhsExpr : Expr) (gate : Gate) :
+    M ReifiedBVLogical := do
   let congrThm := congrThmOfGate gate
   let boolExpr := .gate gate lhs.bvExpr rhs.bvExpr
   let expr :=
@@ -99,6 +100,35 @@ def mkNot (sub : ReifiedBVLogical) (subExpr : Expr) : M ReifiedBVLogical := do
     return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof
   return ⟨boolExpr, proof, expr⟩
 
+/--
+Construct the reified version of `if discrExpr then lhsExpr else rhsExpr`.
+This function assumes that `discrExpr`, lhsExpr` and `rhsExpr` are the corresponding expressions to
+`discr`, `lhs` and `rhs`.
+-/
+def mkIte (discr lhs rhs : ReifiedBVLogical) (discrExpr lhsExpr rhsExpr : Expr) :
+    M ReifiedBVLogical := do
+  let boolExpr := .ite discr.bvExpr lhs.bvExpr rhs.bvExpr
+  let expr :=
+    mkApp4
+      (mkConst ``BoolExpr.ite)
+      (mkConst ``BVPred)
+      discr.expr
+      lhs.expr
+      rhs.expr
+  let proof := do
+    let discrEvalExpr ← ReifiedBVLogical.mkEvalExpr discr.expr
+    let lhsEvalExpr ← ReifiedBVLogical.mkEvalExpr lhs.expr
+    let rhsEvalExpr ← ReifiedBVLogical.mkEvalExpr rhs.expr
+    let discrProof ← discr.evalsAtAtoms
+    let lhsProof ← lhs.evalsAtAtoms
+    let rhsProof ← rhs.evalsAtAtoms
+    return mkApp9
+      (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.ite_congr)
+      discrExpr lhsExpr rhsExpr
+      discrEvalExpr lhsEvalExpr rhsEvalExpr
+      discrProof lhsProof rhsProof
+  return ⟨boolExpr, proof, expr⟩
+
 end ReifiedBVLogical
 
 end Frontend
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
index deb3fb3926e7..a49ed33a87ed 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean
@@ -18,52 +18,55 @@ open Lean.Meta
 
 /--
 This function adds the two lemmas:
-- `boolExpr = true → atomExpr = 1#1`
-- `boolExpr = false → atomExpr = 0#1`
-It assumes that `boolExpr` and `atomExpr` are the expressions corresponding to `bool` and `atom`.
-Furthermore it assumes that `atomExpr` is of the form `BitVec.ofBool boolExpr`.
+- `discrExpr = true → atomExpr = lhsExpr`
+- `discrExpr = false → atomExpr = rhsExpr`
+It assumes that `discrExpr`, `lhsExpr` and `rhsExpr` are the expressions corresponding to `discr`,
+`lhs` and `rhs`. Furthermore it assumes that `atomExpr` is of the form
+`if discrExpr = true then lhsExpr else rhsExpr`.
 -/
-def addOfBoolLemmas (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
-    LemmaM Unit := do
-  let some ofBoolTrueLemma ← mkOfBoolTrueLemma bool atom boolExpr atomExpr | return ()
-  LemmaM.addLemma ofBoolTrueLemma
-  let some ofBoolFalseLemma ← mkOfBoolFalseLemma bool atom boolExpr atomExpr | return ()
-  LemmaM.addLemma ofBoolFalseLemma
+def addIfLemmas (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+    (discrExpr atomExpr lhsExpr rhsExpr : Expr) : LemmaM Unit := do
+  let some trueLemma ← mkIfTrueLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  LemmaM.addLemma trueLemma
+  let some falseLemma ← mkIfFalseLemma discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr | return ()
+  LemmaM.addLemma falseLemma
 where
-  mkOfBoolTrueLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
-      M (Option SatAtBVLogical) := mkOfBoolLemma bool atom boolExpr atomExpr true 1#1
+  mkIfTrueLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
+    mkIfLemma true discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
 
-  mkOfBoolFalseLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr) :
-      M (Option SatAtBVLogical) := mkOfBoolLemma bool atom boolExpr atomExpr false 0#1
+  mkIfFalseLemma (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) :=
+    mkIfLemma false discr atom lhs rhs discrExpr atomExpr lhsExpr rhsExpr
 
-  mkOfBoolLemma (bool : ReifiedBVLogical) (atom : ReifiedBVExpr) (boolExpr atomExpr : Expr)
-     (boolVal : Bool) (resVal : BitVec 1) : M (Option SatAtBVLogical) := do
+  mkIfLemma (discrVal : Bool) (discr : ReifiedBVLogical) (atom lhs rhs : ReifiedBVExpr)
+      (discrExpr atomExpr lhsExpr rhsExpr : Expr) : M (Option SatAtBVLogical) := do
+    let resExpr := if discrVal then lhsExpr else rhsExpr
+    let resValExpr := if discrVal then lhs else rhs
     let lemmaName :=
-      match boolVal with
-      | .true => ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_true
-      | .false => ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_false
+      if discrVal then
+        ``Std.Tactic.BVDecide.Reflect.BitVec.if_true
+      else
+        ``Std.Tactic.BVDecide.Reflect.BitVec.if_false
+    let discrValExpr := toExpr discrVal
+    let discrVal ← ReifiedBVLogical.mkBoolConst discrVal
 
-    let boolValExpr := toExpr boolVal
-    let boolVal ← ReifiedBVLogical.mkBoolConst boolVal
-    let resExpr := toExpr resVal
-    let resValExpr ← ReifiedBVExpr.mkBVConst resVal
+    let eqDiscrExpr ← mkAppM ``BEq.beq #[discrExpr, discrValExpr]
+    let eqDiscr ← ReifiedBVLogical.mkGate discr discrVal discrExpr discrValExpr .beq
 
-    let eqBoolExpr ← mkAppM ``BEq.beq #[boolExpr, boolValExpr]
-    let eqBool ← ReifiedBVLogical.mkGate bool boolVal boolExpr boolValExpr .beq
-
-    let eqBVExpr ← mkAppM ``BEq.beq #[mkApp (mkConst ``BitVec.ofBool) boolExpr, resExpr]
+    let eqBVExpr ← mkAppM ``BEq.beq #[atomExpr, resExpr]
     let some eqBVPred ← ReifiedBVPred.mkBinPred atom resValExpr atomExpr resExpr .eq | return none
     let eqBV ← ReifiedBVLogical.ofPred eqBVPred
 
     let trueExpr := mkConst ``Bool.true
-    let impExpr ← mkArrow (← mkEq eqBoolExpr trueExpr) (← mkEq eqBVExpr trueExpr)
+    let impExpr ← mkArrow (← mkEq eqDiscrExpr trueExpr) (← mkEq eqBVExpr trueExpr)
     let decideImpExpr ← mkAppOptM ``Decidable.decide #[some impExpr, none]
-    let imp ← ReifiedBVLogical.mkGate eqBool eqBV eqBoolExpr eqBVExpr .imp
+    let imp ← ReifiedBVLogical.mkGate eqDiscr eqBV eqDiscrExpr eqBVExpr .imp
 
     let proof := do
       let evalExpr ← ReifiedBVLogical.mkEvalExpr imp.expr
       let congrProof ← imp.evalsAtAtoms
-      let lemmaProof := mkApp (mkConst lemmaName) boolExpr
+      let lemmaProof := mkApp4 (mkConst lemmaName) (toExpr lhs.width) discrExpr lhsExpr rhsExpr
       return mkApp4
         (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.lemma_congr)
         decideImpExpr
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
index dffe381999f3..002ed924088f 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean
@@ -47,8 +47,6 @@ where
       binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr
     | HMod.hMod _ _ _ _ lhsExpr rhsExpr =>
       binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr
-    | BitVec.sdiv _ lhsExpr rhsExpr =>
-      binaryReflection lhsExpr rhsExpr .sdiv ``Std.Tactic.BVDecide.Reflect.BitVec.sdiv_congr
     | Complement.complement _ _ innerExpr =>
       unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr
     | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr =>
@@ -207,11 +205,15 @@ where
         .rotateRight
         ``BVUnOp.rotateRight
         ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr
-    | BitVec.ofBool boolExpr =>
-      let some bool ← ReifiedBVLogical.of boolExpr | return none
-      let atomExpr := (mkApp (mkConst ``BitVec.ofBool) boolExpr)
-      let some atom ← ReifiedBVExpr.bitVecAtom atomExpr | return none
-      addOfBoolLemmas bool atom boolExpr atomExpr
+    | ite _ discrExpr _ lhsExpr rhsExpr =>
+      let_expr Eq α discrExpr val := discrExpr | return none
+      let_expr Bool := α | return none
+      let_expr Bool.true := val | return none
+      let some atom ← ReifiedBVExpr.bitVecAtom x | return none
+      let some discr ← ReifiedBVLogical.of discrExpr | return none
+      let some lhs ← goOrAtom lhsExpr | return none
+      let some rhs ← goOrAtom rhsExpr | return none
+      addIfLemmas discr atom lhs rhs discrExpr x lhsExpr rhsExpr
       return some atom
     | _ => return none
 
@@ -371,6 +373,14 @@ where
       | Bool => gateReflection lhsExpr rhsExpr .beq
       | BitVec _ => goPred t
       | _ => return none
+    | ite _ discrExpr _ lhsExpr rhsExpr =>
+      let_expr Eq α discrExpr val := discrExpr | return none
+      let_expr Bool := α | return none
+      let_expr Bool.true := val | return none
+      let some discr ← goOrAtom discrExpr | return none
+      let some lhs ← goOrAtom lhsExpr | return none
+      let some rhs ← goOrAtom rhsExpr | return none
+      return some (← ReifiedBVLogical.mkIte discr lhs rhs discrExpr lhsExpr rhsExpr)
     | _ => goPred t
 
   /--
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean
index 8d70ba93311d..0ffe2dd63e45 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean
@@ -128,6 +128,8 @@ builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _))
       else
         return .continue
 
+attribute [builtin_bv_normalize_proc↓] reduceIte
+
 /--
 A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes
 the goal fully, indicated by returning `none`.
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
index d809340d14b7..cfcfaf7dbbd4 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
@@ -73,10 +73,6 @@ inductive BVBinOp where
   Unsigned modulo.
   -/
   | umod
-  /--
-  Signed division.
-  -/
-  | sdiv
 
 namespace BVBinOp
 
@@ -88,7 +84,6 @@ def toString : BVBinOp → String
   | mul => "*"
   | udiv => "/ᵤ"
   | umod => "%ᵤ"
-  | sdiv => "/ₛ"
 
 instance : ToString BVBinOp := ⟨toString⟩
 
@@ -103,7 +98,6 @@ def eval : BVBinOp → (BitVec w → BitVec w → BitVec w)
   | mul => (· * ·)
   | udiv => (· / ·)
   | umod => (· % · )
-  | sdiv => BitVec.sdiv
 
 @[simp] theorem eval_and : eval .and = ((· &&& ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_or : eval .or = ((· ||| ·) : BitVec w → BitVec w → BitVec w) := by rfl
@@ -112,7 +106,6 @@ def eval : BVBinOp → (BitVec w → BitVec w → BitVec w)
 @[simp] theorem eval_mul : eval .mul = ((· * ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_udiv : eval .udiv = ((· / ·) : BitVec w → BitVec w → BitVec w) := by rfl
 @[simp] theorem eval_umod : eval .umod = ((· % ·) : BitVec w → BitVec w → BitVec w) := by rfl
-@[simp] theorem eval_sdiv : eval .sdiv = (BitVec.sdiv : BitVec w → BitVec w → BitVec w) := by rfl
 
 end BVBinOp
 
@@ -448,6 +441,8 @@ def eval (assign : BVExpr.Assignment) (expr : BVLogicalExpr) : Bool :=
 @[simp] theorem eval_const : eval assign (.const b) = b := rfl
 @[simp] theorem eval_not : eval assign (.not x) = !eval assign x := rfl
 @[simp] theorem eval_gate : eval assign (.gate g x y) = g.eval (eval assign x) (eval assign y) := rfl
+@[simp] theorem eval_ite :
+  eval assign (.ite d l r) = if (eval assign d) then (eval assign l) else (eval assign r) := rfl
 
 def Sat (x : BVLogicalExpr) (assign : BVExpr.Assignment) : Prop := eval assign x = true
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
index ea9095ff18fe..4e9e5bd87eca 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
@@ -21,7 +21,6 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.SignExtend
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Umod
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sdiv
 
 /-!
 This module contains the implementation of a bitblaster for `BitVec` expressions (`BVExpr`).
@@ -118,13 +117,6 @@ where
           dsimp only at hlaig hraig
           omega
         ⟨res, this⟩
-      | .sdiv =>
-        let res := bitblast.blastSdiv aig ⟨lhs, rhs⟩
-        have := by
-          apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastSdiv)
-          dsimp only at hlaig hraig
-          omega
-        ⟨res, this⟩
     | .un op expr =>
       let ⟨⟨eaig, evec⟩, heaig⟩ := go aig expr
       match op with
@@ -235,7 +227,7 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) :
     rw [AIG.LawfulVecOperator.decl_eq (f := blastConst)]
   | bin lhs op rhs lih rih =>
     match op with
-    | .and | .or | .xor | .add | .mul | .udiv | .umod | .sdiv =>
+    | .and | .or | .xor | .add | .mul | .udiv | .umod =>
       dsimp only [go]
       have := (bitblast.go aig lhs).property
       have := (go (go aig lhs).1.aig rhs).property
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sdiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sdiv.lean
deleted file mode 100644
index 996cc28232d8..000000000000
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sdiv.lean
+++ /dev/null
@@ -1,230 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Std.Sat.AIG.If
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Neg
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
-
-/-!
-This module contains the implementation of a bitblaster for `BitVec.sdiv`. The implemented
-circuit is the reduction to udiv.
--/
-
-namespace Std.Tactic.BVDecide
-
-open Std.Sat
-
-namespace BVExpr
-namespace bitblast
-
-variable [Hashable α] [DecidableEq α]
-
-namespace blastSdiv
-
-structure SignBranchInput (aig : AIG α) (len : Nat) where
-  w : Nat
-  lhs : AIG.RefVec aig w
-  rhs : AIG.RefVec aig w
-  lposRpos : AIG.RefVec aig len
-  lposRneg : AIG.RefVec aig len
-  lnegRpos : AIG.RefVec aig len
-  lnegRneg : AIG.RefVec aig len
-  hnezero : w ≠ 0
-
-def signBranch (aig : AIG α) (input : SignBranchInput aig len) : AIG.RefVecEntry α len :=
-  let ⟨w, lhs, rhs, lposRpos, lposRneg, lnegRpos, lnegRneg, hnezero⟩ := input
-  let res := AIG.RefVec.ite aig ⟨rhs.get (w - 1) (by omega), lposRneg, lposRpos⟩
-  let aig := res.aig
-  let lposHalf := res.vec
-  have := AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite) ..
-  let lhs := lhs.cast this
-  let rhs := rhs.cast this
-  let lnegRneg := lnegRneg.cast this
-  let lnegRpos := lnegRpos.cast this
-
-  let res := AIG.RefVec.ite aig ⟨rhs.get (w - 1) (by omega), lnegRneg, lnegRpos⟩
-  let aig := res.aig
-  let lnegHalf := res.vec
-  have := AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite) ..
-  let lhs := lhs.cast this
-  let lposHalf := lposHalf.cast this
-
-  AIG.RefVec.ite aig ⟨lhs.get (w - 1) (by omega), lnegHalf, lposHalf⟩
-
-instance : AIG.LawfulVecOperator α SignBranchInput signBranch where
-  le_size := by
-    intros
-    unfold signBranch
-    dsimp only
-    apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
-    apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)
-    apply AIG.LawfulVecOperator.le_size (f := AIG.RefVec.ite)
-  decl_eq := by
-    intros
-    unfold signBranch
-    dsimp only
-    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
-    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
-    rw [AIG.LawfulVecOperator.decl_eq (f := AIG.RefVec.ite)]
-    · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
-      assumption
-    · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
-      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := AIG.RefVec.ite)
-      assumption
-
-end blastSdiv
-
-def blastSdiv (aig : AIG α) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry α w :=
-  if h : w = 0 then
-    ⟨aig, h ▸ AIG.RefVec.empty⟩
-  else
-    let ⟨lhs, rhs⟩ := input
-    let res := blastNeg aig lhs
-    let aig := res.aig
-    let negLhs := res.vec
-    have := AIG.LawfulVecOperator.le_size (f := blastNeg) ..
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let res := blastNeg aig rhs
-    let aig := res.aig
-    let negRhs := res.vec
-    have := AIG.LawfulVecOperator.le_size (f := blastNeg) ..
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let negLhs := negLhs.cast this
-
-    let res := blastUdiv aig ⟨lhs, rhs⟩
-    let aig := res.aig
-    let lposRpos := res.vec
-    have := AIG.LawfulVecOperator.le_size (f := blastUdiv) ..
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let negRhs := negRhs.cast this
-    let negLhs := negLhs.cast this
-
-    let res := blastUdiv aig ⟨lhs, negRhs⟩
-    let aig := res.aig
-    let ldivnr := res.vec
-    let res := blastNeg aig ldivnr
-    let aig := res.aig
-    let lposRneg := res.vec
-    have := by
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
-      apply AIG.LawfulVecOperator.le_size (f := blastUdiv)
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let negRhs := negRhs.cast this
-    let negLhs := negLhs.cast this
-    let lposRpos := lposRpos.cast this
-
-    let res := blastUdiv aig ⟨negLhs, rhs⟩
-    let aig := res.aig
-    let nldivr := res.vec
-    let res := blastNeg aig nldivr
-    let aig := res.aig
-    let lnegRpos := res.vec
-    have := by
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
-      apply AIG.LawfulVecOperator.le_size (f := blastUdiv)
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let negRhs := negRhs.cast this
-    let negLhs := negLhs.cast this
-    let lposRpos := lposRpos.cast this
-    let lposRneg := lposRneg.cast this
-
-    let res := blastUdiv aig ⟨negLhs, negRhs⟩
-    let aig := res.aig
-    let lnegRneg := res.vec
-    have := AIG.LawfulVecOperator.le_size (f := blastUdiv) ..
-    let lhs := lhs.cast this
-    let rhs := rhs.cast this
-    let lposRpos := lposRpos.cast this
-    let lposRneg := lposRneg.cast this
-    let lnegRpos := lnegRpos.cast this
-
-    blastSdiv.signBranch aig ⟨w, lhs, rhs, lposRpos, lposRneg, lnegRpos, lnegRneg, h⟩
-
-instance : AIG.LawfulVecOperator α AIG.BinaryRefVec blastSdiv where
-  le_size := by
-    intros
-    unfold blastSdiv
-    dsimp only
-    split
-    · simp
-    · apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastSdiv.signBranch)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv)
-      apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastNeg)
-      apply AIG.LawfulVecOperator.le_size (f := blastNeg)
-  decl_eq := by
-    intros
-    unfold blastSdiv
-    dsimp only
-    split
-    · simp
-    · rw [AIG.LawfulVecOperator.decl_eq (f := blastSdiv.signBranch)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastUdiv)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
-      rw [AIG.LawfulVecOperator.decl_eq (f := blastNeg)]
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-      · apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastUdiv)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastNeg)
-        assumption
-
-end bitblast
-end BVExpr
-
-end Std.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
index a5683651c004..81804adfa9f3 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
@@ -27,6 +27,12 @@ theorem bitblast.go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assig
   | literal => simp [ofBoolExprCached.go]
   | not expr ih => simp [ofBoolExprCached.go, ih]
   | gate g lhs rhs lih rih => cases g <;> simp [ofBoolExprCached.go, Gate.eval, lih, rih]
+  | ite discr lhs rhs dih lih rih =>
+    simp only [ofBoolExprCached.go, Ref.cast_eq, denote_mkIfCached,
+      ofBoolExprCached.go_denote_entry, eval_ite]
+    rw [ofBoolExprCached.go_denote_mem_prefix, ofBoolExprCached.go_denote_mem_prefix]
+    · simp [dih, lih, rih]
+    · simp [Ref.hgate]
 
 theorem denote_bitblast (expr : BVLogicalExpr) (assign : BVExpr.Assignment) :
     ⟦bitblast expr, assign.toAIGAssignment⟧ = expr.eval assign := by
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
index 1475225804ca..6c7d5e29f6d4 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -21,7 +21,6 @@ import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.SignExtend
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Mul
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Sdiv
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
 
 /-!
@@ -219,18 +218,6 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
         · simp [Ref.hgate]
       · intros
         rw [← rih]
-    | sdiv =>
-      simp only [go, eval_bin, BVBinOp.eval_sdiv]
-      apply denote_blastSdiv
-      · intros
-        dsimp only
-        rw [go_denote_mem_prefix]
-        rw [← lih (aig := aig)]
-        · simp
-        · assumption
-        · simp [Ref.hgate]
-      · intros
-        rw [← rih]
   | un op expr ih =>
     cases op with
     | not => simp [go, ih, hidx]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sdiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sdiv.lean
deleted file mode 100644
index 9ba6ed8abe5c..000000000000
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sdiv.lean
+++ /dev/null
@@ -1,201 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-prelude
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Neg
-import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Sdiv
-import Std.Tactic.BVDecide.Normalize.BitVec
-
-/-!
-This module contains the verification of the `BitVec.sdiv` bitblaster from `Impl.Operations.Sdiv`.
--/
-
-namespace Std.Tactic.BVDecide
-
-open Std.Sat
-open Std.Sat.AIG
-
-namespace BVExpr
-namespace bitblast
-
-variable [Hashable α] [DecidableEq α]
-
-namespace blastSdiv
-
-theorem denote_signBranch {aig : AIG α} (input : SignBranchInput aig len) (lhs rhs : BitVec input.w)
-    (lposRpos lposRneg lnegRpos lnegRneg : BitVec len)
-    (hleft : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < input.w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx)
-    (hlprp : ∀ (idx : Nat) (hidx : idx < len), ⟦aig, input.lposRpos.get idx hidx, assign⟧ = lposRpos.getLsbD idx)
-    (hlprn : ∀ (idx : Nat) (hidx : idx < len), ⟦aig, input.lposRneg.get idx hidx, assign⟧ = lposRneg.getLsbD idx)
-    (hlnrp : ∀ (idx : Nat) (hidx : idx < len), ⟦aig, input.lnegRpos.get idx hidx, assign⟧ = lnegRpos.getLsbD idx)
-    (hlnrn : ∀ (idx : Nat) (hidx : idx < len), ⟦aig, input.lnegRneg.get idx hidx, assign⟧ = lnegRneg.getLsbD idx) :
-    ∀ (idx : Nat) (hidx : idx < len),
-      ⟦(signBranch aig input).aig, (signBranch aig input).vec.get idx hidx, assign⟧
-        =
-      (match lhs.msb, rhs.msb with
-      | false, false => lposRpos
-      | false, true => lposRneg
-      | true, false => lnegRpos
-      | true, true => lnegRneg).getLsbD idx
-      := by
-  intros
-  unfold signBranch
-  simp only [ne_eq, RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq]
-  split
-  · next h1 =>
-    rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix] at h1
-    rw [hleft, ← BitVec.msb_eq_getLsbD_last] at h1
-    rw [h1]
-    split
-    · next h2 =>
-      rw [AIG.LawfulVecOperator.denote_mem_prefix] at h2
-      rw [hright, ← BitVec.msb_eq_getLsbD_last] at h2
-      rw [h2]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, hlnrn]
-    · next h2 =>
-      rw [AIG.LawfulVecOperator.denote_mem_prefix] at h2
-      rw [hright, ← BitVec.msb_eq_getLsbD_last, Bool.not_eq_true] at h2
-      rw [h2]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, hlnrp]
-  · next h1 =>
-    rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix] at h1
-    rw [hleft, ← BitVec.msb_eq_getLsbD_last, Bool.not_eq_true] at h1
-    rw [h1]
-    rw [AIG.LawfulVecOperator.denote_mem_prefix]
-    rw [AIG.RefVec.denote_ite]
-    split
-    · next h2 =>
-      rw [hright, ← BitVec.msb_eq_getLsbD_last] at h2
-      rw [h2]
-      simp [hlprn]
-    · next h2 =>
-      rw [hright, ← BitVec.msb_eq_getLsbD_last, Bool.not_eq_true] at h2
-      rw [h2]
-      simp [hlprp]
-
-end blastSdiv
-
-theorem denote_blastSdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bool)
-    (input : BinaryRefVec aig w)
-    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
-    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
-    ∀ (idx : Nat) (hidx : idx < w),
-      ⟦(blastSdiv aig input).aig, (blastSdiv aig input).vec.get idx hidx, assign⟧
-        =
-      (BitVec.sdiv lhs rhs).getLsbD idx := by
-  intros
-  generalize hres : blastSdiv aig input = res
-  unfold blastSdiv at hres
-  split at hres
-  · omega
-  · dsimp only at hres
-    rw [← hres]
-    clear hres
-    rw [blastSdiv.denote_signBranch
-        (lhs := lhs)
-        (rhs := rhs)
-        (lposRpos := lhs / rhs)
-        (lposRneg := -(lhs / (-rhs)))
-        (lnegRpos := -((-lhs) / rhs))
-        (lnegRneg := ((-lhs) / (-rhs)))
-      ]
-    · rw [BitVec.sdiv_eq]
-      rfl
-    · simp only [RefVec.get_cast, Ref.cast_eq]
-      intros
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-      rw [hleft]
-    · simp only [RefVec.get_cast, Ref.cast_eq]
-      intros
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-      rw [hright]
-    · simp only [RefVec.get_cast, Ref.cast_eq]
-      intros
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix]
-      rw [denote_blastUdiv (lhs := lhs) (rhs := rhs)]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp [hleft]
-        · simp [Ref.hgate]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp [hright]
-        · simp [Ref.hgate]
-    · simp only [RefVec.get_cast, Ref.cast_eq]
-      intros
-      rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-        AIG.LawfulVecOperator.denote_mem_prefix]
-      rw [denote_blastNeg (value := lhs / (-rhs))]
-      intros
-      rw [denote_blastUdiv (lhs := lhs) (rhs := -rhs)]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp [hleft]
-        · simp [Ref.hgate]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp only [RefVec.get_cast, Ref.cast_eq]
-          rw [denote_blastNeg (value := rhs)]
-          intros
-          rw [AIG.LawfulVecOperator.denote_mem_prefix]
-          · simp [hright]
-          · simp [Ref.hgate]
-        · simp [Ref.hgate]
-    · simp only [RefVec.get_cast, Ref.cast_eq]
-      intros
-      rw [AIG.LawfulVecOperator.denote_mem_prefix]
-      rw [denote_blastNeg (value := (-lhs) / rhs)]
-      intros
-      rw [denote_blastUdiv (lhs := -lhs) (rhs := rhs)]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp only [RefVec.get_cast, Ref.cast_eq]
-          rw [denote_blastNeg (value := lhs)]
-          simp [hleft]
-        · simp [Ref.hgate]
-      · intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp [hright]
-        · simp [Ref.hgate]
-    · simp only
-      intros
-      rw [denote_blastUdiv (lhs := -lhs) (rhs := - rhs)]
-      · intros
-        simp only [RefVec.get_cast, Ref.cast_eq]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix]
-        rw [denote_blastNeg (value := lhs)]
-        simp [hleft]
-      · intros
-        simp only [RefVec.get_cast, Ref.cast_eq]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix, AIG.LawfulVecOperator.denote_mem_prefix,
-          AIG.LawfulVecOperator.denote_mem_prefix]
-        rw [denote_blastNeg (value := rhs)]
-        intros
-        rw [AIG.LawfulVecOperator.denote_mem_prefix]
-        · simp [hright]
-        · simp [Ref.hgate]
-
-
-end bitblast
-end BVExpr
-
-end Std.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
index e389699cb177..d8b21e6ca115 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean
@@ -41,6 +41,7 @@ inductive BoolExpr (α : Type)
   | const : Bool → BoolExpr α
   | not : BoolExpr α → BoolExpr α
   | gate : Gate → BoolExpr α → BoolExpr α → BoolExpr α
+  | ite : BoolExpr α → BoolExpr α → BoolExpr α → BoolExpr α
 
 namespace BoolExpr
 
@@ -49,28 +50,22 @@ def toString [ToString α] : BoolExpr α → String
   | const b => ToString.toString b
   | not x => "!" ++ toString x
   | gate g x y => "(" ++ toString x ++ " " ++ g.toString ++ " " ++ toString y ++ ")"
+  | ite d l r => "(if " ++ toString d ++ " " ++ toString l ++ " " ++ toString r ++ ")"
 
 instance [ToString α] : ToString (BoolExpr α) := ⟨toString⟩
 
-def size : BoolExpr α → Nat
-  | .literal _
-  | .const _ => 1
-  | .not x => x.size + 1
-  | .gate _ x y => x.size + y.size + 1
-
-theorem size_pos (x : BoolExpr α) : 0 < x.size := by
-  cases x <;> simp [size] <;> omega
-
 def eval (a : α → Bool) : BoolExpr α → Bool
   | .literal l => a l
   | .const b => b
   | .not x => !eval a x
   | .gate g x y => g.eval (eval a x) (eval a y)
+  | .ite d l r => if d.eval a then l.eval a else r.eval a
 
 @[simp] theorem eval_literal : eval a (.literal l) = a l := rfl
 @[simp] theorem eval_const : eval a (.const b) = b := rfl
 @[simp] theorem eval_not : eval a (.not x) = !eval a x := rfl
 @[simp] theorem eval_gate : eval a (.gate g x y) = g.eval (eval a x) (eval a y) := rfl
+@[simp] theorem eval_ite : eval a (.ite d l r) = if d.eval a then l.eval a else r.eval a := rfl
 
 def Sat (a : α → Bool) (x : BoolExpr α) : Prop := eval a x = true
 def Unsat (x : BoolExpr α) : Prop := ∀ f, eval f x = false
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
index d6443b8323a5..3b322aa47840 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
@@ -7,6 +7,7 @@ prelude
 import Std.Sat.AIG.CachedGates
 import Std.Sat.AIG.CachedGatesLemmas
 import Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
+import Std.Sat.AIG.If
 
 /-!
 This module contains the logic to turn a `BoolExpr Nat` into an `AIG` with maximum subterm sharing,
@@ -39,6 +40,21 @@ where
       let ret := aig.mkNotCached exprRef
       have := LawfulOperator.le_size (f := mkNotCached) aig exprRef
       ⟨ret, by dsimp only [ret] at *; omega⟩
+    | .ite discr lhs rhs =>
+      let ⟨⟨aig, discrRef⟩, dextend⟩ := go aig discr atomHandler
+      let ⟨⟨aig, lhsRef⟩, lextend⟩ := go aig lhs atomHandler
+      let ⟨⟨aig, rhsRef⟩, rextend⟩ := go aig rhs atomHandler
+      let discrRef := discrRef.cast <| by
+        dsimp only at lextend rextend ⊢
+        omega
+      let lhsRef := lhsRef.cast <| by
+        dsimp only at rextend ⊢
+        omega
+
+      let input := ⟨discrRef, lhsRef, rhsRef⟩
+      let ret := aig.mkIfCached input
+      have := LawfulOperator.le_size (f := mkIfCached) aig input
+      ⟨ret, by dsimp only [ret] at lextend rextend dextend ⊢; omega⟩
     | .gate g lhs rhs =>
       let ⟨⟨aig, lhsRef⟩, lextend⟩ := go aig lhs atomHandler
       let ⟨⟨aig, rhsRef⟩, rextend⟩ := go aig rhs atomHandler
@@ -64,13 +80,15 @@ where
         have := LawfulOperator.le_size (f := mkImpCached) aig input
         ⟨ret, by dsimp only [ret] at lextend rextend ⊢; omega⟩
 
+namespace ofBoolExprCached
+
 variable (atomHandler : AIG β → α → Entrypoint β) [LawfulOperator β (fun _ => α) atomHandler]
 
-theorem ofBoolExprCached.go_decls_size_le (expr : BoolExpr α) (aig : AIG β) :
+theorem go_le_size (expr : BoolExpr α) (aig : AIG β) :
     aig.decls.size ≤ (ofBoolExprCached.go aig expr atomHandler).val.aig.decls.size :=
   (ofBoolExprCached.go aig expr atomHandler).property
 
-theorem ofBoolExprCached.go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.size) (hbounds) :
+theorem go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.size) (hbounds) :
     (ofBoolExprCached.go aig expr atomHandler).val.aig.decls[idx]'hbounds = aig.decls[idx] := by
   induction expr generalizing aig with
   | const =>
@@ -81,13 +99,22 @@ theorem ofBoolExprCached.go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.si
     rw [AIG.LawfulOperator.decl_eq (f := atomHandler)]
   | not expr ih =>
     simp only [go]
-    have := go_decls_size_le atomHandler expr aig
+    have := go_le_size atomHandler expr aig
     specialize ih aig (by omega) (by omega)
     rw [AIG.LawfulOperator.decl_eq (f := mkNotCached)]
     assumption
+  | ite discr lhs rhs dih lih rih =>
+    have := go_le_size atomHandler discr aig
+    have := go_le_size atomHandler lhs (go aig discr atomHandler).val.aig
+    have := go_le_size atomHandler rhs (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig
+    specialize dih aig (by omega) (by omega)
+    specialize lih (go aig discr atomHandler).val.aig (by omega) (by omega)
+    specialize rih (go (go aig discr atomHandler).val.aig lhs atomHandler).val.aig (by omega) (by omega)
+    simp only [go]
+    rw [AIG.LawfulOperator.decl_eq (f := mkIfCached), rih, lih, dih]
   | gate g lhs rhs lih rih =>
-    have := go_decls_size_le atomHandler lhs aig
-    have := go_decls_size_le atomHandler rhs (go aig lhs atomHandler).val.aig
+    have := go_le_size atomHandler lhs aig
+    have := go_le_size atomHandler rhs (go aig lhs atomHandler).val.aig
     specialize lih aig (by omega) (by omega)
     specialize rih (go aig lhs atomHandler).val.aig (by omega) (by omega)
     cases g with
@@ -104,17 +131,30 @@ theorem ofBoolExprCached.go_decl_eq (idx) (aig : AIG β) (h : idx < aig.decls.si
       simp only [go]
       rw [AIG.LawfulOperator.decl_eq (f := mkImpCached), rih, lih]
 
-theorem ofBoolExprCached.go_isPrefix_aig {aig : AIG β} :
+theorem go_isPrefix_aig {aig : AIG β} :
     IsPrefix aig.decls (go aig expr atomHandler).val.aig.decls := by
   apply IsPrefix.of
   · intro idx h
     apply ofBoolExprCached.go_decl_eq
-  · apply ofBoolExprCached.go_decls_size_le
+  · apply go_le_size
+
+theorem go_denote_mem_prefix :
+    ⟦
+      (go aig expr atomHandler).val.aig,
+      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      assign
+    ⟧
+      =
+    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+  apply go_isPrefix_aig
 
 @[simp]
-theorem ofBoolExprCached.go_denote_entry (entry : Entrypoint β) {h} :
+theorem go_denote_entry (entry : Entrypoint β) {h} :
     ⟦(go entry.aig expr atomHandler).val.aig, ⟨entry.ref.gate, h⟩, assign⟧ = ⟦entry, assign⟧ := by
   apply denote.eq_of_isPrefix
   apply ofBoolExprCached.go_isPrefix_aig
 
+end ofBoolExprCached
+
 end Std.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index 35824b3d76ff..175b2867427d 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -45,6 +45,48 @@ attribute [bv_normalize] BitVec.ofNat_eq_ofNat
 theorem BitVec.ofNatLt_reduce (n : Nat) (h) : BitVec.ofNatLt n h = BitVec.ofNat w n := by
   simp [BitVec.ofNatLt, BitVec.ofNat, Fin.ofNat', Nat.mod_eq_of_lt h]
 
+@[bv_normalize]
+theorem BitVec.ofBool_eq_if (b : Bool) : BitVec.ofBool b = if b then 1#1 else 0#1 := by
+  revert b
+  decide
+
+@[bv_normalize]
+theorem BitVec.sdiv_udiv (x y : BitVec w) :
+    x.sdiv y =
+      if x.msb then
+        if y.msb then
+          (-x) / (-y)
+        else
+          -((-x) / y)
+      else
+        if y.msb then
+          -(x / (-y))
+        else
+          x / y := by
+  rw [BitVec.sdiv_eq]
+  cases x.msb <;> cases y.msb <;> simp
+
+@[bv_normalize]
+theorem BitVec.smod_umod (x y : BitVec w) :
+    x.smod y =
+      if x.msb then
+        if y.msb then
+          - ((- x).umod (- y))
+        else
+          let u := (- x).umod y
+          (if u = 0#w then u else y - u)
+      else
+        if y.msb then
+          let u := x.umod (- y)
+          (if u = 0#w then u else u + y)
+        else
+          x.umod y := by
+  rw [BitVec.smod_eq]
+  cases x.msb <;> cases y.msb <;> simp
+
+attribute [bv_normalize] Bool.cond_eq_if
+attribute [bv_normalize] BitVec.abs_eq
+
 end Reduce
 
 section Constant
@@ -59,8 +101,6 @@ attribute [bv_normalize] BitVec.getLsbD_concat_zero
 attribute [bv_normalize] BitVec.mul_one
 attribute [bv_normalize] BitVec.one_mul
 attribute [bv_normalize] BitVec.not_not
-attribute [bv_normalize] BitVec.ofBool_true
-attribute [bv_normalize] BitVec.ofBool_false
 
 end Constant
 
@@ -258,7 +298,6 @@ attribute [bv_normalize] BitVec.zero_umod
 attribute [bv_normalize] BitVec.umod_zero
 attribute [bv_normalize] BitVec.umod_one
 attribute [bv_normalize] BitVec.umod_eq_and
-attribute [bv_normalize] BitVec.sdiv_eq_and
 
 end Normalize
 end Std.Tactic.BVDecide
diff --git a/src/Std/Tactic/BVDecide/Normalize/Bool.lean b/src/Std/Tactic/BVDecide/Normalize/Bool.lean
index 38f4ec6cc957..061c9c3fded4 100644
--- a/src/Std/Tactic/BVDecide/Normalize/Bool.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/Bool.lean
@@ -40,6 +40,8 @@ attribute [bv_normalize] Bool.xor_not_self
 attribute [bv_normalize] Bool.not_not
 attribute [bv_normalize] Bool.and_self_left
 attribute [bv_normalize] Bool.and_self_right
+attribute [bv_normalize] eq_self
+attribute [bv_normalize] ite_self
 
 @[bv_normalize]
 theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide
diff --git a/src/Std/Tactic/BVDecide/Reflect.lean b/src/Std/Tactic/BVDecide/Reflect.lean
index 09142cd69b1f..6507c6b7c355 100644
--- a/src/Std/Tactic/BVDecide/Reflect.lean
+++ b/src/Std/Tactic/BVDecide/Reflect.lean
@@ -118,19 +118,13 @@ theorem umod_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' =
     (lhs' % rhs') = (lhs % rhs) := by
   simp[*]
 
-theorem sdiv_congr (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (BitVec.sdiv lhs' rhs') = (BitVec.sdiv lhs rhs) := by
-  simp[*]
-
-theorem ofBool_true (b : Bool) :
-    decide ((b == true) = true → (BitVec.ofBool b == 1#1) = true) = true := by
-  revert b
-  decide
+theorem if_true (discr : Bool) (lhs rhs : BitVec w) :
+    decide ((discr == true) = true → ((if discr = true then lhs else rhs) == lhs) = true) = true := by
+  cases discr <;> simp
 
-theorem ofBool_false (b : Bool) :
-    decide ((b == false) = true → (BitVec.ofBool b == 0#1) = true) = true := by
-  revert b
-  decide
+theorem if_false (discr : Bool) (lhs rhs : BitVec w) :
+    decide ((discr == false) = true → ((if discr = true then lhs else rhs) == rhs) = true) = true := by
+  cases discr <;> simp
 
 end BitVec
 
@@ -155,6 +149,11 @@ theorem imp_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
     (decide (lhs' → rhs')) = (decide (lhs → rhs)) := by
   simp[*]
 
+theorem ite_congr (discr lhs rhs discr' lhs' rhs' : Bool) (h1 : discr' = discr) (h2 : lhs' = lhs)
+    (h3 : rhs' = rhs) :
+    (if discr' = true then lhs' else rhs') = (if discr = true then lhs else rhs) := by
+  simp[*]
+
 theorem false_of_eq_true_of_eq_false (h₁ : x = true) (h₂ : x = false) : False := by
   cases h₁; cases h₂
 
diff --git a/src/Std/Tactic/BVDecide/Syntax.lean b/src/Std/Tactic/BVDecide/Syntax.lean
index aeedb45f0464..bbfaa1e0ca6b 100644
--- a/src/Std/Tactic/BVDecide/Syntax.lean
+++ b/src/Std/Tactic/BVDecide/Syntax.lean
@@ -26,11 +26,7 @@ syntax (name := bvCheck) "bv_check " str : tactic
 /--
 Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and
 verifying it inside Lean. The solvable goals are currently limited to the Lean equivalent of
-[`QF_BV`](https://smt-lib.org/logics-all.shtml#QF_BV) with the following changes:
-- Division and remainder operations are not yet implemented.
-- if-then-else is not yet implemented.
-- `BitVec.ofBool` is not yet implemented.
-
+[`QF_BV`](https://smt-lib.org/logics-all.shtml#QF_BV):
 ```lean
 example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
   intros
diff --git a/tests/lean/run/bv_arith.lean b/tests/lean/run/bv_arith.lean
index 310b5fb64f1a..db01746eaf12 100644
--- a/tests/lean/run/bv_arith.lean
+++ b/tests/lean/run/bv_arith.lean
@@ -51,3 +51,12 @@ theorem arith_unit_11 (x y : BitVec 8) (hx : x.msb = false) (hy : y.msb = false)
 
 theorem arith_unit_12 (x y : BitVec 8) (hx : x.msb = false) (hy : y.msb = true) : -(x / -y) = x.sdiv y := by
   bv_decide
+
+theorem arith_unit_13 (x y : BitVec 8) (hx : x.msb = false) (hy : y.msb = false) : x.umod y = x.smod y := by
+  bv_decide
+
+theorem arith_unit_14 (x y : BitVec 8) (hx : x.msb = true) (hy : y.msb = true) : (-((-x).umod (-y))) = x.smod y := by
+  bv_decide
+
+theorem arith_unit_15 (x : BitVec 32) : BitVec.sle x (BitVec.abs x) := by
+  bv_decide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index c9cc36676968..92d699311fb6 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -78,7 +78,9 @@ example {x : BitVec 16} : (10 + x) + 2 = 12 + x := by bv_normalize
 example {x : BitVec 16} : (x + 10) + 2 = 12 + x := by bv_normalize
 example {x : BitVec 16} : 2 + (x + 10) = 12 + x := by bv_normalize
 example {x : BitVec 16} : 2 + (10 + x) = 12 + x := by bv_normalize
-example {x y : BitVec 1} : x.sdiv y = x &&& y := by bv_normalize
+example {x : BitVec 16} {b : Bool} : (if b then x else x) = x := by bv_normalize
+example {b : Bool} {x : Bool} : (bif b then x else x) = x := by bv_normalize
+example {x : BitVec 16} : x.abs = if x.msb then -x else x := by bv_normalize
 
 section
 
diff --git a/tests/lean/run/bv_substructure.lean b/tests/lean/run/bv_substructure.lean
index 44cf860a22a3..3ecf37924227 100644
--- a/tests/lean/run/bv_substructure.lean
+++ b/tests/lean/run/bv_substructure.lean
@@ -27,3 +27,15 @@ theorem substructure_unit_4 (a b : Bool) : (a && b) = (b && a) := by
 
 theorem substructure_unit_5 (a : Bool) (b c : BitVec 32) (h1 : b < c ↔ a) (h2 : a = true) : b < c := by
   bv_decide
+
+theorem substructure_unit_6 (a b c: Bool) : (if a then b else c) = (if !a then c else b) := by
+  bv_decide
+
+theorem substructure_unit_7 (a b c: Bool) : (bif a then b else c) = (bif !a then c else b) := by
+  bv_decide
+  
+theorem substructure_unit_8 (x : BitVec 32) : (if x.getLsbD 0 then !x.getLsbD 0 else x.getLsbD 0) = false := by
+  bv_decide
+
+theorem substructure_unit_9 (x y : BitVec 32) (h : x.getLsbD 0 = false) : (if x.getLsbD 0 then x else y) = y := by
+  bv_decide