diff --git a/testcases/BinarySearch.scala b/testcases/BinarySearch.scala
index 5ee63b316c6e254e113696ac0b53c15b9e7ff70e..986ee41ae6a057065bc8520c5af010092b67b2b2 100644
--- a/testcases/BinarySearch.scala
+++ b/testcases/BinarySearch.scala
@@ -23,9 +23,10 @@ object BinarySearch {
         low = i + 1
     }) invariant(
         res >= -1 &&
-        res > a.length &&
+        res < a.length &&
         0 <= low && 
         low <= high + 1 && 
+        high >= -1 &&
         high < a.length && 
         (if (res >= 0) 
             a(res) == key else