From aa04b90a509becea16ce04bd315d6909f72132e4 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Fri, 25 Oct 2024 16:12:09 -0700
Subject: [PATCH] chore: update lean-toolchain, consequently add sdiv support

We mirror the implementation of udiv and umod,
where we check for the special case when width = 0
and return 0.
---
 Leanwuzla.lean | 9 +++++++++
 lean-toolchain | 2 +-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/Leanwuzla.lean b/Leanwuzla.lean
index 7881369..6e2de35 100644
--- a/Leanwuzla.lean
+++ b/Leanwuzla.lean
@@ -112,6 +112,15 @@ where
       | .xor => pushBinaryOp "bvxor" lhs rhs
       | .add => pushBinaryOp "bvadd" lhs rhs
       | .mul => pushBinaryOp "bvmul" lhs rhs
+      | .sdiv =>
+        let zero := goBVExpr <| .const (w := w) 0
+        withParens do
+          push "ite "
+          pushBinaryOp "=" zero rhs
+          push " "
+          zero
+          push " "
+          pushBinaryOp "bvsdiv" lhs rhs
       | .udiv =>
         let zero := goBVExpr <| .const (w := w) 0
         withParens do
diff --git a/lean-toolchain b/lean-toolchain
index f3a11d3..d23cac2 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-10-12
+leanprover/lean4:nightly-2024-10-24