Commit 63907e17 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Fix bench

parent 6e11331f
......@@ -6847,7 +6847,6 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb
= value q (sx - sy + 1) * value y sy
+ value r sy }
ensures { value r sy < value y sy }
diverges
=
let uone = (1:UInt32.uint32) in
let nx = malloc (UInt32.(+) (UInt32.of_int32 sx) uone) in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment