From 5e2a7724439a573ec9b47232d727e903c6d9c8d3 Mon Sep 17 00:00:00 2001
From: Jeehoon Kang <jeehoon.kang@kaist.ac.kr>
Date: Wed, 28 Sep 2022 21:17:01 +0900
Subject: [PATCH] Fix binary search type

---
 assets/why3/binary_search.mlw | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/assets/why3/binary_search.mlw b/assets/why3/binary_search.mlw
index c2df74f..eca628a 100644
--- a/assets/why3/binary_search.mlw
+++ b/assets/why3/binary_search.mlw
@@ -11,7 +11,7 @@ module BinarySearch
   use import ref.Ref
   use import array.Array
 
-  let binary_search (a : array int) (v : int)
+  let binary_search (a : array int) (v : int) : int
     requires { forall i1 i2 : int. 0 <= i1 < i2 < length a -> a[i1] <= a[i2] }
     ensures  { 0 <= result <= length a }
     ensures  { forall i: int. 0 <= i < result -> a[i] < v }