diff --git a/testcases/BinarySearchFun.scala b/testcases/BinarySearchFun.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1398f9b9e4c6b31af646c0d3c5e89fafdd23dbab
--- /dev/null
+++ b/testcases/BinarySearchFun.scala
@@ -0,0 +1,59 @@
+import leon.Utils._
+
+object BinarySearchFun {
+
+  def binarySearch(a: Array[Int], key: Int, low: Int, high: Int): Int = ({
+    require(a.length > 0 && sorted(a, low, high) &&
+        0 <= low && low <= high + 1 && high < a.length
+    )
+
+    if(low <= high) {
+      val i = (high + low) / 2
+      val v = a(i)
+
+      if(v == key) i
+      else if (v > key) binarySearch(a, key, low, i - 1)
+      else binarySearch(a, key, i + 1, high)
+    } else -1
+  }) ensuring(res =>
+      res >= -1 &&
+      res < a.length &&
+      (if (res >= 0)
+          a(res) == key else
+          (high < 0 || (!occurs(a, low, (high+low)/2, key) && !occurs(a, (high+low)/2, high, key)))
+      )
+    )
+
+
+  def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+    require(a.length >= 0 && to <= a.length && from >= 0)
+    def rec(i: Int): Boolean = {
+      require(i >= 0)
+      if(i >= to)
+        false
+      else {
+       if(a(i) == key) true else rec(i+1)
+      }
+    }
+    if(from >= to)
+      false
+    else
+      rec(from)
+  }
+
+
+  def sorted(a: Array[Int], l: Int, u: Int) : Boolean = {
+    require(a.length >= 0 && l >= 0 && l <= u + 1 && u < a.length)
+    val t = sortedWhile(true, l, l, u, a)
+    t._1
+  }
+
+  def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Array[Int]): (Boolean, Int) = {
+    require(a.length >= 0 && l >= 0 && l <= u+1 && u < a.length && k >= l && k <= u + 1)
+    if(k < u) {
+      sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a)
+    } else (isSorted, k)
+  }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/BubbleFun.scala b/testcases/BubbleFun.scala
index 5962eea28e93cbd3d496ae9c7dd92af3a1297d15..4847fc8acf0e756b3af6d8f5bad84ff2c83b2406 100644
--- a/testcases/BubbleFun.scala
+++ b/testcases/BubbleFun.scala
@@ -19,7 +19,7 @@ object BubbleFun {
         val t = sortNestedWhile(sortedArray, 0, i, size)
         sortWhile(t._2, t._1, i - 1, size)
       } else (j, sortedArray, i)
-    }) ensuring(res => isArray(res._2, size) && 
+    }) ensuring(res => isArray(res._2, size) &&
                        sorted(res._2, size, res._3, size - 1) &&
                        partitioned(res._2, size, 0, res._3, res._3+1, size-1) &&
                        res._3 >= 0 && res._3 <= 0 /*&& content(res._2, size) == content(sortedArray, size)*/
@@ -32,7 +32,7 @@ object BubbleFun {
               partitioned(sortedArray, size, 0, i, i+1, size-1) &&
               partitioned(sortedArray, size, 0, j-1, j, j))
       if(j < i) {
-        val newSortedArray = 
+        val newSortedArray =
           if(sortedArray(j) > sortedArray(j + 1))
             sortedArray.updated(j, sortedArray(j + 1)).updated(j+1, sortedArray(j))
           else
@@ -91,7 +91,7 @@ object BubbleFun {
     // ------------- partitioned ------------------
     def partitioned(a: Map[Int,Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int) : Boolean = {
       require(isArray(a, size) && size < 5 && l1 >= 0 && u1 < l2 && u2 < size)
-      if(l2 > u2 || l1 > u1) 
+      if(l2 > u2 || l1 > u1)
         true
       else {
         val t = partitionedWhile(l2, true, l1, l1, size, u2, l2, u1, a)
@@ -114,20 +114,20 @@ object BubbleFun {
           (if (a(i) > a(j))
             false
           else
-            isPartitionned), 
+            isPartitionned),
           j + 1, i, l1, u1, size, u2, a, l2)
       } else (isPartitionned, j)
     }
 
 
     //------------ isArray -------------------
-    def isArray(a: Map[Int,Int], size: Int): Boolean = 
+    def isArray(a: Map[Int,Int], size: Int): Boolean =
       if(size <= 0)
         false
       else
         isArrayRec(0, size, a)
 
-    def isArrayRec(i: Int, size: Int, a: Map[Int,Int]): Boolean = 
+    def isArrayRec(i: Int, size: Int, a: Map[Int,Int]): Boolean =
       if (i >= size)
         true
       else {
@@ -141,13 +141,15 @@ object BubbleFun {
     // ----------------- content ------------------
     def content(a: Map[Int, Int], size: Int): Set[Int] = {
       require(isArray(a, size) && size < 5)
-      var i = 0
-      var s = Set.empty[Int]
-      while(i < size) {
-        s = s ++ Set(a(i))
-        i = i + 1
-      }
-      s
+      contentRec(a, size, 0)
+    }
+
+    def contentRec(a: Map[Int, Int], size: Int, i: Int): Set[Int] = {
+      require(isArray(a, size) && i >= 0)
+      if(i < size)
+        Set(a(i)) ++ contentRec(a, size, i+1)
+      else
+        Set.empty[Int]
     }
 
 }