Made merge sort verify using better specified splitAtIndex.

library/par/package.scala

@@ -9,6 +9,7 @@ import leon.lang.synthesis.choose
 package object par {
 
   // @library
+  @inline
   def parallel[A,B](x: => A, y: => B) : (A,B) = {
     (x,y)
   }

testcases/verification/list-algorithms/BasicMergeSort.scala

@@ -18,7 +18,8 @@ object MergeSort {
   def msort[T](less: (T, T) => Boolean)(l: List[T]): List[T] = {
     if (l.size <= 1) l
     else {
-      val (first, second) = l.evenSplit
+      val c = l.length/2
+      val (first, second) = l.splitAtIndex(c) // evenSplit
       merge(less)(msort(less)(first), msort(less)(second))
     }
   } ensuring { res => res.content == l.content && res.size == l.size }

testcases/verification/list-algorithms/BasicMergeSortPar.scala

@@ -19,9 +19,11 @@ object MergeSortPar {
   def msort[T](less: (T, T) => Boolean)(l: List[T]): List[T] = {
     if (l.size <= 1) l
     else {
-      val (first, second) = l.evenSplit
+      val c = l.length/2
+      val (first, second) = l.splitAtIndex(c) // evenSplit
       val (s1, s2) = parallel(msort(less)(first), msort(less)(second))
       merge(less)(s1, s2)
     }
-  } ensuring { res => res.content == l.content && res.size == l.size }
+  } ensuring { res => res.content == l.content && 
+                      res.size == l.size }
 }