Fix this benchmark

testcases/verification/list-algorithms/MergeSort.scala

 import leon.lang._
-import leon.annotation._
+import synthesis._
+import leon.collection._
 
 object MergeSort {
-  sealed abstract class List
-  case class Cons(head:Int,tail:List) extends List
-  case class Nil() extends List
 
-  case class Pair(fst:List,snd:List)
-
-  def contents(l: List): Set[Int] = l match {
-    case Nil() => Set.empty
-    case Cons(x,xs) => contents(xs) ++ Set(x)
+  def isSorted(l: List[BigInt]): Boolean = l match {
+    case Cons(x, t@Cons(y, _)) => x <= y && isSorted(t)
+    case _ => true
   }
 
-  def is_sorted(l: List): Boolean = l match {
-    case Nil() => true
-    case Cons(x,xs) => xs match {
-      case Nil() => true
-      case Cons(y, ys) => x <= y && is_sorted(Cons(y, ys))
+  def merge(l1: List[BigInt], l2: List[BigInt]): List[BigInt] = {
+    require(isSorted(l1) && isSorted(l2))
+    (l1, l2) match {
+      case (Nil(), _) => l2
+      case (_, Nil()) => l1
+      case (Cons(h1,t1), Cons(h2, t2)) =>
+        if (h1 <= h2) Cons(h1, merge(t1, l2))
+        else          Cons(h2, merge(l1, t2))
     }
+  } ensuring { 
+    (res: List[BigInt]) =>
+      isSorted(res) && 
+      res.content == l1.content ++ l2.content &&
+      res.size == l1.size + l2.size
   }
 
-  def length(list:List): Int = list match {
-    case Nil() => 0
-    case Cons(x,xs) => 1 + length(xs)
-  }
-
-  def splithelper(aList:List,bList:List,n:Int): Pair =
-    if (n <= 0) Pair(aList,bList)
-    else
-    bList match {
-              case Nil() => Pair(aList,bList)
-              case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+  def split(l: List[BigInt]): (List[BigInt], List[BigInt]) = {
+    l match {
+      case Cons(h1, Cons(h2, tail)) =>
+        val (rec1, rec2) = split(tail)
+        (h1 :: rec1, h2 :: rec2)
+      case _ => (l, Nil[BigInt]())
     }
+  } ensuring { (res: (List[BigInt], List[BigInt])) =>
+    val (r1, r2) = res
+    r1.size + r2.size == l.size &&
+    r1.content ++ r2.content == l.content &&
+    r1.size - r2.size <= 1 &&
+    r2.size - r1.size <= 1
+  }
 
-  def split(list:List,n:Int): Pair = splithelper(Nil(),list,n)
-
-  def merge(aList:List, bList:List):List = (bList match {
-    case Nil() => aList
-    case Cons(x,xs) =>
-         aList match {
-           case Nil() => bList
-           case Cons(y,ys) =>
-                if (y < x)
-               Cons(y,merge(ys, bList))
-            else
-           Cons(x,merge(aList, xs))
-     }
-  }) ensuring(res => contents(res) == contents(aList) ++ contents(bList))
-
-  def mergeSort(list:List):List = (list match {
-    case Nil() => list
-    case Cons(x,Nil()) => list
-    case _ =>
-         val p = split(list,length(list)/2)
-     merge(mergeSort(p.fst), mergeSort(p.snd))
-  }) ensuring(res => contents(res) == contents(list) && is_sorted(res))
-
+  def mergeSort(l: List[BigInt]): List[BigInt] = {
+    val (l1, l2) = split(l)
+    merge(mergeSort(l1), mergeSort(l2))
+  } ensuring ( res =>
+    isSorted(res) && 
+    res.content == l.content &&
+    res.size == l.size
+  )
 
-  @ignore
-  def main(args: Array[String]): Unit = {
-    val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
-    println(ls)
-    println(mergeSort(ls))
-  }
 }