Merge pull request #2 from opencompl/sdiv

chore: update lean-toolchain, consequently add sdiv support
hargoniX · Oct 26, 2024 · ca72cbe · ca72cbe
2 parents a51af40 + aa04b90
commit ca72cbe
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