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