Moved mkInfiniteTree example to demo file.

testcases/BinarySearchTree.scala

@@ -133,6 +133,12 @@ object BinarySearchTree {
       }) ensuring (contents(_) == contents(tree) -- Set(value))
   */
 
+  def mkInfiniteTree(x: Int): Node = {
+    Node(mkInfiniteTree(x), x, mkInfiniteTree(x))
+  } ensuring (res =>
+    res.left != Leaf() && res.right != Leaf()
+  )
+
   def contains(tree: Tree, value: Int): Boolean = tree match {
     case Leaf() => false
     case n@Node(l, v, r) => if (v < value) {

testcases/UnificationTest.scala

@@ -43,14 +43,6 @@ object UnificationTest {
   })*/
   
   
-  
-  // Proved by unifier
-  def mkInfiniteTree(x: Int): Node = {
-    Node(mkInfiniteTree(x), x, mkInfiniteTree(x))
-  } ensuring (res =>
-    res.left != Leaf() && res.right != Leaf()
-  )
-  
   // Cannot be solved yet, due to the presence of an if expression
   def insert(tree: Tree, value: Int) : Node = (tree match {
     case Leaf() => Node(Leaf(), value, Leaf())