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.
hargoniX · Oct 25, 2024 · aa04b90 · aa04b90
1 parent a51af40
commit aa04b90
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git 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
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-10-12
+leanprover/lean4:nightly-2024-10-24