diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index f156cdac4f2a..7a1395adfd14 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -29,6 +29,7 @@ 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
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
index 3df04f164842..64c2f9552de7 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean
@@ -102,6 +102,8 @@ 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 =>
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
index 48637e6eb2bd..d809340d14b7 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean
@@ -73,6 +73,10 @@ inductive BVBinOp where
   Unsigned modulo.
   -/
   | umod
+  /--
+  Signed division.
+  -/
+  | sdiv
 
 namespace BVBinOp
 
@@ -84,6 +88,7 @@ def toString : BVBinOp → String
   | mul => "*"
   | udiv => "/ᵤ"
   | umod => "%ᵤ"
+  | sdiv => "/ₛ"
 
 instance : ToString BVBinOp := ⟨toString⟩
 
@@ -98,6 +103,7 @@ 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
@@ -106,6 +112,7 @@ 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
 
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 4e9e5bd87eca..ea9095ff18fe 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
@@ -21,6 +21,7 @@ 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`).
@@ -117,6 +118,13 @@ 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
@@ -227,7 +235,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 =>
+    | .and | .or | .xor | .add | .mul | .udiv | .umod | .sdiv =>
       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
new file mode 100644
index 000000000000..996cc28232d8
--- /dev/null
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sdiv.lean
@@ -0,0 +1,230 @@
+/-
+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/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
index 6c7d5e29f6d4..1475225804ca 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -21,6 +21,7 @@ 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
 
 /-!
@@ -218,6 +219,18 @@ 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
new file mode 100644
index 000000000000..9ba6ed8abe5c
--- /dev/null
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sdiv.lean
@@ -0,0 +1,201 @@
+/-
+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/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index f2a4d4ad61ae..95c2a7ce3c44 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -262,6 +262,7 @@ 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/Reflect.lean b/src/Std/Tactic/BVDecide/Reflect.lean
index aebaba3b7b00..93e729b537ed 100644
--- a/src/Std/Tactic/BVDecide/Reflect.lean
+++ b/src/Std/Tactic/BVDecide/Reflect.lean
@@ -118,6 +118,10 @@ 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[*]
+
 end BitVec
 
 namespace Bool
diff --git a/tests/lean/run/bv_arith.lean b/tests/lean/run/bv_arith.lean
index 32855c0b5276..310b5fb64f1a 100644
--- a/tests/lean/run/bv_arith.lean
+++ b/tests/lean/run/bv_arith.lean
@@ -45,3 +45,9 @@ theorem arith_unit_10 (x y : BitVec 8) : x % y ≤ x := by
 
 theorem arith_unit_10' (x y : BitVec 8) : x.umod y ≤ x := by
   bv_decide
+
+theorem arith_unit_11 (x y : BitVec 8) (hx : x.msb = false) (hy : y.msb = false) : x / y = x.sdiv y := by
+  bv_decide
+
+theorem arith_unit_12 (x y : BitVec 8) (hx : x.msb = false) (hy : y.msb = true) : -(x / -y) = x.sdiv y := by
+  bv_decide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 0d4c7c2a0708..90982c1af2b6 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -78,9 +78,7 @@ 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
 
 section