From 3a463b55b16318cc4404d5ee5d954f067b969d6c Mon Sep 17 00:00:00 2001
From: Jeehoon Kang <jeehoon.kang@kaist.ac.kr>
Date: Wed, 28 Sep 2022 23:15:39 +0900
Subject: [PATCH] Strengthen the post-condition

---
 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 2d222bc..e00e19f 100644
--- a/assets/why3/binary_search.mlw
+++ b/assets/why3/binary_search.mlw
@@ -15,7 +15,7 @@ module BinarySearch
     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 }
-    ensures  { result < length a -> a[result] >= v }
+    ensures  { forall i: int. result <= i < length a -> v <= a[i] }
   =
     (* IMPORTANT: DON'T MODIFY THE ABOVE LINES *)
     0 (* TODO *)