diff --git a/testcases/synthesis/cav2013/Sorting.scala b/testcases/synthesis/cav2013/Sorting.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d396c5eb700a8e9002b5b11a2e289382bb93c4a1
--- /dev/null
+++ b/testcases/synthesis/cav2013/Sorting.scala
@@ -0,0 +1,204 @@
+import leon.Annotations._
+import leon.Utils._
+
+// Sorting lists is a fundamental problem in CS.
+object Sorting {
+ // Data types
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class LList
+ case class LCons(head : List, tail : LList) extends LList
+ case class LNil() extends LList
+
+ // Abstraction functions
+ def content(list : List) : Set[Int] = list match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def lContent(llist : LList) : Set[Int] = llist match {
+ case LNil() => Set.empty[Int]
+ case LCons(x, xs) => content(x) ++ lContent(xs)
+ }
+
+ def size(list : List) : Int = (list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil() => true
+ case Cons(_, Nil()) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def lIsSorted(llist : LList) : Boolean = llist match {
+ case LNil() => true
+ case LCons(x, xs) => isSorted(x) && lIsSorted(xs)
+ }
+
+ def abs(i : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ /***************************
+ * *
+ * I N S E R T I O N *
+ * *
+ ***************************/
+
+ def insertSpec(elem : Int, list : List, res : List) : Boolean = {
+ isSorted(list) && // Part of precondition, really.
+ isSorted(res) && content(res) == content(list) ++ Set(elem)
+ }
+
+ // This will require:
+ // 1) Propagation of path-conditions.
+ // 2) Something like "inequality-split".
+ def insert(elem : Int, list : List) : List = {
+ require(isSorted(list))
+ choose { (res : List) => insertSpec(elem, list, res) }
+ }
+
+ def insertImpl(elem : Int, list : List) : List = {
+ require(isSorted(list))
+ list match {
+ case Nil() => Cons(elem, Nil())
+ case c @ Cons(x, _) if(elem <= x) => Cons(elem, c)
+ case Cons(x, xs) => Cons(x, insertImpl(elem, xs))
+ }
+ } ensuring(insertSpec(elem, list, _))
+
+ /**********************************
+ * *
+ * M E R G I N G (slow+fast) *
+ * *
+ **********************************/
+
+ def mergeSpec(list1 : List, list2 : List, res : List) : Boolean = {
+ // isSorted(list1) && isSorted(list2) && // Part of precondition, really.
+ isSorted(res) && content(res) == content(list1) ++ content(list2)
+ }
+
+ // The goal is that the synthesizer figures out that it should use insert.
+ // Currently, CEGIS with functions is too slow to handle that benchmark,
+ // even when insertImpl is the only function in the scope.
+ // (Note that I already propagated the path condition.)
+ // If you put mergeImpl in the scope, it solves it (how surprising).
+ def merge(list1 : List, list2 : List) : List = {
+ require(isSorted(list1) && isSorted(list2))
+ choose { (res : List) => mergeSpec(list1, list2, res) }
+ }
+
+ def mergeImpl(list1 : List, list2 : List) : List = {
+ require(isSorted(list1) && isSorted(list2))
+
+ list1 match {
+ case Nil() => list2
+ case Cons(x, xs) => insertImpl(x, mergeImpl(xs, list2))
+ }
+ } ensuring(res => mergeSpec(list1, list2, res))
+
+ def mergeFastImpl(list1 : List, list2 : List) : List = {
+ require(isSorted(list1) && isSorted(list2))
+
+ (list1, list2) match {
+ case (_, Nil()) => list1
+ case (Nil(), _) => list2
+ case (Cons(x, xs), Cons(y, ys)) =>
+ if(x <= y) {
+ Cons(x, mergeFastImpl(xs, list2))
+ } else {
+ Cons(y, mergeFastImpl(list1, ys))
+ }
+ }
+ } ensuring(res => mergeSpec(list1, list2, res))
+
+ /***************************
+ * *
+ * S P L I T T I N G *
+ * *
+ ***************************/
+
+ def splitSpec(list : List, res : (List,List)) : Boolean = {
+ val s1 = size(res._1)
+ val s2 = size(res._2)
+ abs(s1 - s2) <= 1 && s1 + s2 == size(list) &&
+ content(res._1) ++ content(res._2) == content(list)
+ }
+
+ // I think this one is really close to working. I suspect it would work
+ // if the generators in CEGIS had a way to read from tuples. E.g. if
+ // t of type (Int,Int) is in context, t._1 and t._2 should be candidates
+ // for integers.
+ //
+ // (Note that if you weaken splitSpec in any way, you get valid and
+ // useless answers).
+ def split(list : List) : (List,List) = {
+ choose { (res : (List,List)) => splitSpec(list, res) }
+ }
+
+ def splitImpl(list : List) : (List,List) = (list match {
+ case Nil() => (Nil(), Nil())
+ case Cons(x, Nil()) => (Cons(x, Nil()), Nil())
+ case Cons(x1, Cons(x2, xs)) =>
+ val (s1,s2) = splitImpl(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ }) ensuring(res => splitSpec(list, res))
+
+ /***********************
+ * *
+ * S O R T I N G *
+ * *
+ ***********************/
+
+ def sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+ def insertionSortImpl(in : List) : List = (in match {
+ case Nil() => Nil()
+ case Cons(x, xs) => insertImpl(x, insertionSortImpl(xs))
+ }) ensuring(res => sortSpec(in, res))
+
+ // Not really quicksort, neither mergesort.
+ def weirdSortImpl(in : List) : List = (in match {
+ case Nil() => Nil()
+ case Cons(x, Nil()) => Cons(x, Nil())
+ case _ =>
+ val (s1,s2) = splitImpl(in)
+ mergeFastImpl(weirdSortImpl(s1), weirdSortImpl(s2))
+ }) ensuring(res => sortSpec(in, res))
+
+ def toLList(list : List) : LList = (list match {
+ case Nil() => LNil()
+ case Cons(x, xs) => LCons(Cons(x, Nil()), toLList(xs))
+ }) ensuring(res => lContent(res) == content(list) && lIsSorted(res))
+
+ def mergeMap(llist : LList) : LList = {
+ require(lIsSorted(llist))
+
+ llist match {
+ case LNil() => LNil()
+ case o @ LCons(x, LNil()) => o
+ case LCons(x, LCons(y, ys)) => LCons(mergeFastImpl(x, y), mergeMap(ys))
+ }
+ } ensuring(res => lContent(res) == lContent(llist) && lIsSorted(res))
+
+ def mergeReduce(llist : LList) : List = {
+ require(lIsSorted(llist))
+
+ llist match {
+ case LNil() => Nil()
+ case LCons(x, LNil()) => x
+ case _ => mergeReduce(mergeMap(llist))
+ }
+ } ensuring(res => content(res) == lContent(llist) && isSorted(res))
+
+ def mergeSortImpl(in : List) : List = {
+ mergeReduce(toLList(in))
+ } ensuring(res => sortSpec(in, res))
+}