diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index a8116240bfb4d5af4d5d8dee9bee6ed2e3040457..463ae6c026c2a0899010e0ead630ea940bcce3f4 100644
--- a/testcases/BinarySearchTree.scala
+++ b/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) {
diff --git a/testcases/UnificationTest.scala b/testcases/UnificationTest.scala
index 60f06c4e42113b86368f615cd960713f34d3aab8..2202a573d29133c3f9ce158a8d30e557e6f46493 100644
--- a/testcases/UnificationTest.scala
+++ b/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())