From 57598155062c8d106ecd84933a5382e6c1a1de02 Mon Sep 17 00:00:00 2001
From: Jeehoon Kang <jeehoon.kang@kaist.ac.kr>
Date: Mon, 12 Sep 2022 13:35:14 +0900
Subject: [PATCH] Add a warning on binary search

---
 assets/why3/binary_search.mlw | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/assets/why3/binary_search.mlw b/assets/why3/binary_search.mlw
index d85c134..c2df74f 100644
--- a/assets/why3/binary_search.mlw
+++ b/assets/why3/binary_search.mlw
@@ -17,7 +17,6 @@ module BinarySearch
     ensures  { forall i: int. 0 <= i < result -> a[i] < v }
     ensures  { result < length a -> a[result] >= v }
   =
-    let l = ref (-1) in
-    let u = ref (length a) in
-    !u - !l (* TODO *)
+    (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
+    0 (* TODO *)
 end