Fix mergeSort in list algorithms

testcases/verification/list-algorithms/MergeSort.scala

@@ -26,7 +26,12 @@ object MergeSort {
   }
 
   def split(l: List[BigInt]): (List[BigInt], List[BigInt]) = {
+    require(l.size > 1)
     l match {
+      case Cons(h1, Cons(h2, Nil())) =>
+        (List(h1), List(h2))
+      case Cons(h1, Cons(h2, Cons(h3, Nil()))) =>
+        (List(h1, h3), List(h2))
       case Cons(h1, Cons(h2, tail)) =>
         val (rec1, rec2) = split(tail)
         (h1 :: rec1, h2 :: rec2)
@@ -34,15 +39,16 @@ object MergeSort {
     }
   } ensuring { (res: (List[BigInt], List[BigInt])) =>
     val (r1, r2) = res
+    r1.size < l.size && r2.size < l.size &&
     r1.size + r2.size == l.size &&
-    r1.content ++ r2.content == l.content &&
-    r1.size - r2.size <= 1 &&
-    r2.size - r1.size <= 1
+    r1.content ++ r2.content == l.content
   }
 
   def mergeSort(l: List[BigInt]): List[BigInt] = {
-    val (l1, l2) = split(l)
-    merge(mergeSort(l1), mergeSort(l2))
+    if (l.size <= 1) l else {
+      val (l1, l2) = split(l)
+      merge(mergeSort(l1), mergeSort(l2))
+    }
   } ensuring ( res =>
     isSorted(res) && 
     res.content == l.content &&