diff --git a/library/par/package.scala b/library/par/package.scala index 4690eddbff16d5c756335195ed1c1ed9193833f5..6e8d1d571b8b21f63a725353a4db30ee92fdeb0d 100644 --- a/library/par/package.scala +++ b/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) } diff --git a/testcases/verification/list-algorithms/BasicMergeSort.scala b/testcases/verification/list-algorithms/BasicMergeSort.scala index 474f768a5a10b32eec99e6eebacfd3680d6ccda2..55e632ff8f68307ba24cff691bde6b45fa206842 100644 --- a/testcases/verification/list-algorithms/BasicMergeSort.scala +++ b/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 } diff --git a/testcases/verification/list-algorithms/BasicMergeSortPar.scala b/testcases/verification/list-algorithms/BasicMergeSortPar.scala index e5620482d87cd48dee2fe74f7c2e1bcda5b473df..493122b2f8d0cc6356ef76b3ba6cfaf33e66c38a 100644 --- a/testcases/verification/list-algorithms/BasicMergeSortPar.scala +++ b/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 } }