From ea4edf23598a1f5945741cfd6d90e41b21a52ad6 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 4 Apr 2013 15:16:51 +0200
Subject: [PATCH] Add various synthesis benchmarks

---
 testcases/synthesis/cav2013/Sorting.scala     |  85 ++++++++-
 .../oopsla2013/BinaryTree/Complete.scala      |  76 ++++++++
 .../oopsla2013/BinaryTree/Delete.scala        |  46 +++++
 .../oopsla2013/BinaryTree/Diff.scala          |  64 +++++++
 .../oopsla2013/BinaryTree/Insert.scala        |  28 +++
 .../oopsla2013/BinaryTree/Union.scala         |  55 ++++++
 .../synthesis/oopsla2013/Church/Add.scala     |  24 +++
 .../oopsla2013/Church/Complete.scala          |  43 +++++
 .../oopsla2013/Church/Distinct.scala          |  37 ++++
 .../synthesis/oopsla2013/Church/Mult.scala    |  37 ++++
 .../synthesis/oopsla2013/Church/Squared.scala |  44 +++++
 .../synthesis/oopsla2013/List/Complete.scala  |  74 ++++++++
 .../synthesis/oopsla2013/List/Delete.scala    |  40 ++++
 .../synthesis/oopsla2013/List/Diff.scala      |  58 ++++++
 .../synthesis/oopsla2013/List/Insert.scala    |  27 +++
 .../synthesis/oopsla2013/List/Union.scala     |  49 +++++
 .../oopsla2013/SortedList/Complete.scala      | 171 ++++++++++++++++++
 .../oopsla2013/SortedList/Delete.scala        |  80 ++++++++
 .../oopsla2013/SortedList/Diff.scala          | 101 +++++++++++
 .../oopsla2013/SortedList/Insert1.scala       |  47 +++++
 .../oopsla2013/SortedList/Insert2.scala       |  47 +++++
 .../oopsla2013/SortedList/Sort.scala          | 142 +++++++++++++++
 .../oopsla2013/SortedList/Split.scala         | 128 +++++++++++++
 .../oopsla2013/SortedList/Split1.scala        | 128 +++++++++++++
 .../oopsla2013/SortedList/Split2.scala        | 128 +++++++++++++
 .../oopsla2013/SortedList/Split3.scala        | 128 +++++++++++++
 .../oopsla2013/SortedList/Union.scala         |  91 ++++++++++
 .../oopsla2013/SparseVector/Complete.scala    | 114 ++++++++++++
 .../oopsla2013/SparseVector/Delete.scala      |  89 +++++++++
 .../oopsla2013/SparseVector/Get.scala         | 106 +++++++++++
 .../oopsla2013/SparseVector/Set.scala         |  72 ++++++++
 .../StrictSortedList/Complete.scala           |  99 ++++++++++
 .../oopsla2013/StrictSortedList/Delete.scala  |  63 +++++++
 .../oopsla2013/StrictSortedList/Diff.scala    |  84 +++++++++
 .../oopsla2013/StrictSortedList/Insert.scala  |  47 +++++
 .../oopsla2013/StrictSortedList/Union.scala   |  73 ++++++++
 36 files changed, 2721 insertions(+), 4 deletions(-)
 create mode 100644 testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
 create mode 100644 testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
 create mode 100644 testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
 create mode 100644 testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
 create mode 100644 testcases/synthesis/oopsla2013/BinaryTree/Union.scala
 create mode 100644 testcases/synthesis/oopsla2013/Church/Add.scala
 create mode 100644 testcases/synthesis/oopsla2013/Church/Complete.scala
 create mode 100644 testcases/synthesis/oopsla2013/Church/Distinct.scala
 create mode 100644 testcases/synthesis/oopsla2013/Church/Mult.scala
 create mode 100644 testcases/synthesis/oopsla2013/Church/Squared.scala
 create mode 100644 testcases/synthesis/oopsla2013/List/Complete.scala
 create mode 100644 testcases/synthesis/oopsla2013/List/Delete.scala
 create mode 100644 testcases/synthesis/oopsla2013/List/Diff.scala
 create mode 100644 testcases/synthesis/oopsla2013/List/Insert.scala
 create mode 100644 testcases/synthesis/oopsla2013/List/Union.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Complete.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Delete.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Diff.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Insert1.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Insert2.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Sort.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Split.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Split1.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Split2.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Split3.scala
 create mode 100644 testcases/synthesis/oopsla2013/SortedList/Union.scala
 create mode 100644 testcases/synthesis/oopsla2013/SparseVector/Complete.scala
 create mode 100644 testcases/synthesis/oopsla2013/SparseVector/Delete.scala
 create mode 100644 testcases/synthesis/oopsla2013/SparseVector/Get.scala
 create mode 100644 testcases/synthesis/oopsla2013/SparseVector/Set.scala
 create mode 100644 testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
 create mode 100644 testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
 create mode 100644 testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
 create mode 100644 testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
 create mode 100644 testcases/synthesis/oopsla2013/StrictSortedList/Union.scala

diff --git a/testcases/synthesis/cav2013/Sorting.scala b/testcases/synthesis/cav2013/Sorting.scala
index d396c5eb7..c9bee62a0 100644
--- a/testcases/synthesis/cav2013/Sorting.scala
+++ b/testcases/synthesis/cav2013/Sorting.scala
@@ -40,6 +40,11 @@ object Sorting {
     case LCons(x, xs) => isSorted(x) && lIsSorted(xs)
   }
 
+  @induct
+  def sortedLemma(a: Int, x: Int, b: List) = {
+    !(isSorted(Cons(a,b)) && (content(b) contains x)) || (x >= a)
+  } holds
+
   def abs(i : Int) : Int = {
     if(i < 0) -i else i
   } ensuring(_ >= 0)
@@ -51,18 +56,54 @@ object Sorting {
    ***************************/
 
   def insertSpec(elem : Int, list : List, res : List) : Boolean = {
-    isSorted(list) && // Part of precondition, really.
+//    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) }
   }
 
+    //require(head < elem && isSorted(Cons(head, tail)) && r == insertImpl(elem, tail))
+    //require(head < elem && isSorted(Cons(head, tail)) && isSorted(r) && content(r) == content(tail) ++ Set(elem))
+  // head3;tail3;r4;elem4, ((head3 < elem4) ∧ isSorted(Cons(head3, tail3)) ∧ insertSpec(elem4, tail3, r4)) ≺  ⟨ insertSpec(elem4, Cons(head3, tail3), res) ⟩ res 
+  def insertV(head: Int, tail: List, r: List, rh: Int, rt: List, elem: Int) = {
+    require(head < elem && isSorted(Cons(head, tail)) && content(tail) == content(r) && isSorted(r) && r == Cons(rh, rt) && sortedLemma(head, rh, r))
+
+    //insertSpec(elem, Cons(head, tail), Cons(head, r))
+    //rh >= head
+    isSorted(Cons(head, r))
+
+  } holds
+
+    //require(head < elem && isSorted(Cons(head, tail)) && isSorted(r) && content(r) == content(tail) ++ Set(elem))
+  // head3;tail3;r4;elem4, ((head3 < elem4) ∧ isSorted(Cons(head3, tail3)) ∧ insertSpec(elem4, tail3, r4)) ≺  ⟨ insertSpec(elem4, Cons(head3, tail3), res) ⟩ res 
+  def insertV2(head: Int, tail: List, r: List, rh: Int, rt: List, elem: Int) = {
+    require(head < elem && isSorted(Cons(head, tail)) && r == insertImpl(elem, tail) && r == Cons(rh, rt))
+
+    //insertSpec(elem, Cons(head, tail), Cons(head, r))
+    rh >= head
+
+  } holds
+
+  def insert2(elem : Int, list : List) : List = {
+    require(isSorted(list))
+    list match {
+      case Cons(h, t) =>
+        val r = insert2(elem, t)
+        if (elem > h) {
+          choose { (res : List) => insertSpec(elem, Cons(h,t), res) }
+        } else if (elem < h) {
+          Cons(elem, Cons(h, t))
+        } else {
+          Cons(h, t)
+        }
+      case Nil() =>
+        Cons(elem, Nil())
+    }
+  } ensuring { res => insertSpec(elem, list, res) }
+
   def insertImpl(elem : Int, list : List) : List = {
     require(isSorted(list))
     list match {
@@ -159,6 +200,42 @@ object Sorting {
     content(out) == content(in) && isSorted(out)
   }
 
+  def insertSorted(in: List, v: Int): List = {
+    require(isSorted(in));
+
+    in match {
+      case Cons(h, t) =>
+        val r = insertSorted(t, v)
+        if (h < v) {
+          Cons(h, r)
+        } else if (h > v) {
+          Cons(v, Cons(h, t))
+        } else {
+          Cons(h, t)
+        }
+      case _ =>
+        Cons(v, Nil())
+    }
+  } ensuring { res => isSorted(res) && content(res) == content(in) ++ Set(v) }
+
+  def insertSorted1(in: List, v: Int): List = {
+    require(isSorted(in));
+
+    in match {
+      case Cons(h, t) =>
+        val r = insertSorted(t, v)
+        if (h < v) {
+          choose { (res: List) => isSorted(res) && content(res) == content(in) ++ Set(v) }
+        } else if (h > v) {
+          Cons(v, Cons(h, t))
+        } else {
+          Cons(h, t)
+        }
+      case _ =>
+        Cons(v, Nil())
+    }
+  } ensuring { res => isSorted(res) && content(res) == content(in) ++ Set(v) }
+
   def insertionSortImpl(in : List) : List = (in match {
     case Nil() => Nil()
     case Cons(x, xs) => insertImpl(x, insertionSortImpl(xs))
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala b/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
new file mode 100644
index 000000000..51aebf173
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
@@ -0,0 +1,76 @@
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+  sealed abstract class Tree
+  case class Node(left : Tree, value : Int, right : Tree) extends Tree
+  case object Leaf extends Tree
+
+  def content(t : Tree): Set[Int] = t match {
+    case Leaf => Set()
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def size(t: Tree): Int = {
+    t match {
+      case Leaf => 0
+      case Node(l, v, r) => size(l) + size(r) + 1
+    }
+  } ensuring { _ >= 0 }
+
+  def insert(in: Tree, v: Int): Tree = {
+    Node(in, v, Leaf)
+  } ensuring { res => content(res) == content(in) ++ Set(v) }
+
+  //def insert(in: Tree, v: Int): Tree = choose {
+  //  (res: Tree) => content(res) == content(in) ++ Set(v)
+  //}
+
+  def delete(in: Tree, v: Int): Tree = {
+    in match {
+      case Node(l, vv, r) =>
+        if (vv == v) {
+          delete(l, v) match {
+            case Node(ll, lv, lr) =>
+              Node(Node(ll, lv, lr), lv, delete(r, v))
+            case Leaf =>
+              delete(r, v)
+          }
+        } else {
+          Node(delete(l, v), vv, delete(r, v))
+        }
+      case Leaf =>
+        Leaf
+    }
+  } ensuring { res => content(res) == content(in) -- Set(v) }
+
+  //def delete(in: Tree, v: Int): Tree = choose {
+  //  (res: Tree) => content(res) == content(in) -- Set(v)
+  //}
+
+  def union(in1: Tree, in2: Tree): Tree = {
+    in1 match {
+      case Node(l1, v1, r1) =>
+        insert(union(r1, union(l1, in2)), v1)
+      case Leaf =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) }
+
+  //def union(in1: Tree, in2: Tree): Tree = choose {
+  //  (res: Tree) => content(res) == content(in1) ++ content(in2)
+  //}
+
+  def diff(in1: Tree, in2: Tree): Tree = {
+    in2 match {
+      case Node(l2, v2, r2) =>
+        delete(diff(diff(in1, l2), r2), v2)
+      case Leaf =>
+        in1
+    }
+  } ensuring { res => content(res) == content(in1) -- content(in2) }
+
+  //def diff(in1: Tree, in2: Tree): Tree = choose {
+  //  (res: Tree) => content(res) == content(in1) -- content(in2)
+  //}
+}
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala b/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
new file mode 100644
index 000000000..219b3efab
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
@@ -0,0 +1,46 @@
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+  sealed abstract class Tree
+  case class Node(left : Tree, value : Int, right : Tree) extends Tree
+  case object Leaf extends Tree
+
+  def content(t : Tree): Set[Int] = t match {
+    case Leaf => Set()
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def size(t: Tree): Int = {
+    t match {
+      case Leaf => 0
+      case Node(l, v, r) => size(l) + size(r) + 1
+    }
+  } ensuring { _ >= 0 }
+
+  def insert(in: Tree, v: Int): Tree = {
+    Node(in, v, Leaf)
+  } ensuring { res => content(res) == content(in) ++ Set(v) }
+
+  // def delete(in: Tree, v: Int): Tree = {
+  //   in match {
+  //     case Node(l, vv, r) =>
+  //       if (vv == v) {
+  //         delete(l, v) match {
+  //           case Node(ll, lv, lr) =>
+  //             Node(Node(ll, lv, lr), lv, delete(r, v))
+  //           case Leaf =>
+  //             delete(r, v)
+  //         }
+  //       } else {
+  //         Node(delete(l, v), vv, delete(r, v))
+  //       }
+  //     case Leaf =>
+  //       Leaf
+  //   }
+  // } ensuring { res => content(res) == content(in) -- Set(v) }
+
+  def delete(in: Tree, v: Int): Tree = choose {
+    (res: Tree) => content(res) == content(in) -- Set(v)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala b/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
new file mode 100644
index 000000000..bd31f758a
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
@@ -0,0 +1,64 @@
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+  sealed abstract class Tree
+  case class Node(left : Tree, value : Int, right : Tree) extends Tree
+  case object Leaf extends Tree
+
+  def content(t : Tree): Set[Int] = t match {
+    case Leaf => Set()
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def size(t: Tree): Int = {
+    t match {
+      case Leaf => 0
+      case Node(l, v, r) => size(l) + size(r) + 1
+    }
+  } ensuring { _ >= 0 }
+
+  def insert(in: Tree, v: Int): Tree = {
+    Node(in, v, Leaf)
+  } ensuring { res => content(res) == content(in) ++ Set(v) }
+
+  def delete(in: Tree, v: Int): Tree = {
+    in match {
+      case Node(l, vv, r) =>
+        if (vv == v) {
+          delete(l, v) match {
+            case Node(ll, lv, lr) =>
+              Node(Node(ll, lv, lr), lv, delete(r, v))
+            case Leaf =>
+              delete(r, v)
+          }
+        } else {
+          Node(delete(l, v), vv, delete(r, v))
+        }
+      case Leaf =>
+        Leaf
+    }
+  } ensuring { res => content(res) == content(in) -- Set(v) }
+
+  def union(in1: Tree, in2: Tree): Tree = {
+    in1 match {
+      case Node(l1, v1, r1) =>
+        insert(union(r1, union(l1, in2)), v1)
+      case Leaf =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) }
+
+  // def diff(in1: Tree, in2: Tree): Tree = {
+  //   in2 match {
+  //     case Node(l2, v2, r2) =>
+  //       delete(diff(diff(in1, l2), r2), v2)
+  //     case Leaf =>
+  //       in1
+  //   }
+  // } ensuring { res => content(res) == content(in1) -- content(in2) }
+
+  def diff(in1: Tree, in2: Tree): Tree = choose {
+    (res: Tree) => content(res) == content(in1) -- content(in2)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala b/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
new file mode 100644
index 000000000..32291ad3e
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
@@ -0,0 +1,28 @@
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+  sealed abstract class Tree
+  case class Node(left : Tree, value : Int, right : Tree) extends Tree
+  case object Leaf extends Tree
+
+  def content(t : Tree): Set[Int] = t match {
+    case Leaf => Set()
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def size(t: Tree): Int = {
+    t match {
+      case Leaf => 0
+      case Node(l, v, r) => size(l) + size(r) + 1
+    }
+  } ensuring { _ >= 0 }
+
+  //def insert(in: Tree, v: Int): Tree = {
+  //  Node(in, v, Leaf)
+  //} ensuring { res => content(res) == content(in) ++ Set(v) }
+
+  def insert(in: Tree, v: Int): Tree = choose {
+    (res: Tree) => content(res) == content(in) ++ Set(v)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Union.scala b/testcases/synthesis/oopsla2013/BinaryTree/Union.scala
new file mode 100644
index 000000000..c6252a2b7
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Union.scala
@@ -0,0 +1,55 @@
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+  sealed abstract class Tree
+  case class Node(left : Tree, value : Int, right : Tree) extends Tree
+  case object Leaf extends Tree
+
+  def content(t : Tree): Set[Int] = t match {
+    case Leaf => Set()
+    case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+  }
+
+  def size(t: Tree): Int = {
+    t match {
+      case Leaf => 0
+      case Node(l, v, r) => size(l) + size(r) + 1
+    }
+  } ensuring { _ >= 0 }
+
+  def insert(in: Tree, v: Int): Tree = {
+    Node(in, v, Leaf)
+  } ensuring { res => content(res) == content(in) ++ Set(v) }
+
+  def delete(in: Tree, v: Int): Tree = {
+    in match {
+      case Node(l, vv, r) =>
+        if (vv == v) {
+          delete(l, v) match {
+            case Node(ll, lv, lr) =>
+              Node(Node(ll, lv, lr), lv, delete(r, v))
+            case Leaf =>
+              delete(r, v)
+          }
+        } else {
+          Node(delete(l, v), vv, delete(r, v))
+        }
+      case Leaf =>
+        Leaf
+    }
+  } ensuring { res => content(res) == content(in) -- Set(v) }
+
+  // def union(in1: Tree, in2: Tree): Tree = {
+  //   in1 match {
+  //     case Node(l1, v1, r1) =>
+  //       insert(union(r1, union(l1, in2)), v1)
+  //     case Leaf =>
+  //       in2
+  //   }
+  // } ensuring { res => content(res) == content(in1) ++ content(in2) }
+
+  def union(in1: Tree, in2: Tree): Tree = choose {
+    (res: Tree) => content(res) == content(in1) ++ content(in2)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Add.scala b/testcases/synthesis/oopsla2013/Church/Add.scala
new file mode 100644
index 000000000..7b1b6b95f
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Add.scala
@@ -0,0 +1,24 @@
+import leon.Utils._
+object ChurchNumerals {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n:Num) : Int = {
+    n match {
+      case Z => 0
+      case S(p) => 1 + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  // def add(x : Num, y : Num) : Num = (x match {
+  //   case Z => y
+  //   case S(p) => add(p, S(y))
+  // }) ensuring (value(_) == value(x) + value(y))
+
+  def add(x: Num, y: Num): Num = {
+    choose { (r : Num) =>
+      value(r) == value(x) + value(y)
+    }
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Complete.scala b/testcases/synthesis/oopsla2013/Church/Complete.scala
new file mode 100644
index 000000000..c446c789d
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Complete.scala
@@ -0,0 +1,43 @@
+import leon.Utils._
+object ChurchNumerals {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n:Num) : Int = {
+    n match {
+      case Z => 0
+      case S(p) => 1 + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x : Num, y : Num) : Num = (x match {
+    case Z => y
+    case S(p) => add(p, S(y))
+  }) ensuring (value(_) == value(x) + value(y))
+
+  //def add(x: Num, y: Num): Num = {
+  //  choose { (r : Num) =>
+  //    value(r) == value(x) + value(y)
+  //  }
+  //}
+
+  def distinct(x : Num, y : Num) : Num = (x match {
+    case Z =>
+      S(y)
+
+    case S(p) =>
+      y match {
+        case Z =>
+          S(x)
+        case S(p) =>
+          Z
+      }
+  }) ensuring (res => res != x  && res != y)
+
+  // def distinct(x: Num, y: Num): Num = {
+  //   choose { (r : Num) =>
+  //     r != x && r != y
+  //   }
+  // }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Distinct.scala b/testcases/synthesis/oopsla2013/Church/Distinct.scala
new file mode 100644
index 000000000..a7a0189c2
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Distinct.scala
@@ -0,0 +1,37 @@
+import leon.Utils._
+object ChurchNumerals {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n:Num) : Int = {
+    n match {
+      case Z => 0
+      case S(p) => 1 + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x : Num, y : Num) : Num = (x match {
+    case Z => y
+    case S(p) => add(p, S(y))
+  }) ensuring (value(_) == value(x) + value(y))
+
+  //def distinct(x : Num, y : Num) : Num = (x match {
+  //  case Z =>
+  //    S(y)
+
+  //  case S(p) =>
+  //    y match {
+  //      case Z =>
+  //        S(x)
+  //      case S(p) =>
+  //        Z
+  //    }
+  //}) ensuring (res => res != x  && res != y)
+
+  def distinct(x: Num, y: Num): Num = {
+    choose { (r : Num) =>
+      r != x && r != y
+    }
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Mult.scala b/testcases/synthesis/oopsla2013/Church/Mult.scala
new file mode 100644
index 000000000..42519e663
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Mult.scala
@@ -0,0 +1,37 @@
+import leon.Utils._
+object ChurchNumerals {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n:Num) : Int = {
+    n match {
+      case Z => 0
+      case S(p) => 1 + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x : Num, y : Num) : Num = (x match {
+    case Z => y
+    case S(p) => add(p, S(y))
+  }) ensuring (value(_) == value(x) + value(y))
+
+  //def distinct(x : Num, y : Num) : Num = (x match {
+  //  case Z =>
+  //    S(y)
+
+  //  case S(p) =>
+  //    y match {
+  //      case Z =>
+  //        S(x)
+  //      case S(p) =>
+  //        Z
+  //    }
+  //}) ensuring (res => res != x  && res != y)
+
+  def mult(x: Num, y: Num): Num = {
+    choose { (r : Num) =>
+      value(r) == value(x) * value(y)
+    }
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Squared.scala b/testcases/synthesis/oopsla2013/Church/Squared.scala
new file mode 100644
index 000000000..096f212a6
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Squared.scala
@@ -0,0 +1,44 @@
+import leon.Utils._
+object ChurchNumerals {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n:Num) : Int = {
+    n match {
+      case Z => 0
+      case S(p) => 1 + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x : Num, y : Num) : Num = (x match {
+    case Z => y
+    case S(p) => add(p, S(y))
+  }) ensuring (value(_) == value(x) + value(y))
+
+  //def distinct(x : Num, y : Num) : Num = (x match {
+  //  case Z =>
+  //    S(y)
+
+  //  case S(p) =>
+  //    y match {
+  //      case Z =>
+  //        S(x)
+  //      case S(p) =>
+  //        Z
+  //    }
+  //}) ensuring (res => res != x  && res != y)
+
+  def mult(x: Num, y: Num): Num = (y match {
+    case S(p) =>
+      add(mult(x, p), x)
+    case Z =>
+      Z
+  }) ensuring { value(_) == value(x) * value(y) }
+
+  def squared(x: Num): Num = {
+    choose { (r : Num) =>
+      value(r) == value(x) * value(x)
+    }
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/List/Complete.scala b/testcases/synthesis/oopsla2013/List/Complete.scala
new file mode 100644
index 000000000..2f6d74b81
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Complete.scala
@@ -0,0 +1,74 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: Int): List = {
+    Cons(v, in1)
+  } ensuring { content(_) == content(in1) ++ Set(v) }
+
+  //def insert(in1: List, v: Int) = choose {
+  //  (out : List) =>
+  //    content(out) == content(in1) ++ Set(v)
+  //}
+
+  def delete(in1: List, v: Int): List = {
+    in1 match {
+      case Cons(h,t) =>
+        if (h == v) {
+          delete(t, v)
+        } else {
+          Cons(h, delete(t, v))
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { content(_) == content(in1) -- Set(v) }
+
+  //def delete(in1: List, v: Int) = choose {
+  //  (out : List) =>
+  //    content(out) == content(in1) -- Set(v)
+  //}
+
+  def union(in1: List, in2: List): List = {
+    in1 match {
+      case Cons(h, t) =>
+        Cons(h, union(t, in2))
+      case Nil =>
+        in2
+    }
+  } ensuring { content(_) == content(in1) ++ content(in2) }
+
+  //def union(in1: List, in2: List) = choose {
+  //  (out : List) =>
+  //    content(out) == content(in1) ++ content(in2)
+  //}
+
+  def diff(in1: List, in2: List): List = {
+    in2 match {
+      case Nil =>
+        in1
+      case Cons(h, t) =>
+        diff(delete(in1, h), t)
+    }
+  } ensuring { content(_) == content(in1) -- content(in2) }
+
+  //def diff(in1: List, in2: List) = choose {
+  //  (out : List) =>
+  //    content(out) == content(in1) -- content(in2)
+  //}
+
+}
diff --git a/testcases/synthesis/oopsla2013/List/Delete.scala b/testcases/synthesis/oopsla2013/List/Delete.scala
new file mode 100644
index 000000000..9fdef981b
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Delete.scala
@@ -0,0 +1,40 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Delete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: Int): List = {
+    Cons(v, in1)
+  } ensuring { content(_) == content(in1) ++ Set(v) }
+
+  //def delete(in1: List, v: Int): List = {
+  //  in1 match {
+  //    case Cons(h,t) =>
+  //      if (h == v) {
+  //        delete(t, v)
+  //      } else {
+  //        Cons(h, delete(t, v))
+  //      }
+  //    case Nil =>
+  //      Nil
+  //  }
+  //} ensuring { content(_) == content(in1) -- Set(v) }
+
+  def delete(in1: List, v: Int) = choose {
+    (out : List) =>
+      content(out) == content(in1) -- Set(v)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/List/Diff.scala b/testcases/synthesis/oopsla2013/List/Diff.scala
new file mode 100644
index 000000000..3e7121eb1
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Diff.scala
@@ -0,0 +1,58 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Diff {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: Int): List = {
+    Cons(v, in1)
+  } ensuring { content(_) == content(in1) ++ Set(v) }
+
+  def delete(in1: List, v: Int): List = {
+    in1 match {
+      case Cons(h,t) =>
+        if (h == v) {
+          delete(t, v)
+        } else {
+          Cons(h, delete(t, v))
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { content(_) == content(in1) -- Set(v) }
+
+  def union(in1: List, in2: List): List = {
+    in1 match {
+      case Cons(h, t) =>
+        Cons(h, union(t, in2))
+      case Nil =>
+        in2
+    }
+  } ensuring { content(_) == content(in1) ++ content(in2) }
+
+  // def diff(in1: List, in2: List): List = {
+  //   in2 match {
+  //     case Nil =>
+  //       in1
+  //     case Cons(h, t) =>
+  //       diff(delete(in1, h), t)
+  //   }
+  // } ensuring { content(_) == content(in1) -- content(in2) }
+
+  def diff(in1: List, in2: List) = choose {
+    (out : List) =>
+      content(out) == content(in1) -- content(in2)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/List/Insert.scala b/testcases/synthesis/oopsla2013/List/Insert.scala
new file mode 100644
index 000000000..e5b21b45d
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Insert.scala
@@ -0,0 +1,27 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Insert {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  //def insert(in1: List, v: Int): List = {
+  //  Cons(v, in1)
+  //} ensuring { content(_) == content(in1) ++ Set(v) }
+
+  def insert(in1: List, v: Int) = choose {
+    (out : List) =>
+      content(out) == content(in1) ++ Set(v)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/List/Union.scala b/testcases/synthesis/oopsla2013/List/Union.scala
new file mode 100644
index 000000000..adcc943fd
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Union.scala
@@ -0,0 +1,49 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Union {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: Int): List = {
+    Cons(v, in1)
+  } ensuring { content(_) == content(in1) ++ Set(v) }
+
+  def delete(in1: List, v: Int): List = {
+    in1 match {
+      case Cons(h,t) =>
+        if (h == v) {
+          delete(t, v)
+        } else {
+          Cons(h, delete(t, v))
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { content(_) == content(in1) -- Set(v) }
+
+  // def union(in1: List, in2: List): List = {
+  //   in1 match {
+  //     case Cons(h, t) =>
+  //       Cons(h, union(t, in2))
+  //     case Nil =>
+  //       in2
+  //   }
+  // } ensuring { content(_) == content(in1) ++ content(in2) }
+
+  def union(in1: List, in2: List) = choose {
+    (out : List) =>
+      content(out) == content(in1) ++ content(in2)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Complete.scala b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
new file mode 100644
index 000000000..b83a876a3
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
@@ -0,0 +1,171 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert1(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert1(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  //def insert1(in1: List, v: Int) = choose {
+  //  (out : List) =>
+  //    isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+  //}
+
+  def insert2(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          Cons(v, in1)
+        } else {
+          Cons(h, insert2(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
+
+  //def insert2(in1: List, v: Int) = choose {
+  //  (out : List) =>
+  //    isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+  //}
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          delete(t, v)
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  //def delete(in1: List, v: Int) = choose {
+  //  (out : List) =>
+  //    isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+  //}
+
+  def union(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in1 match {
+      case Cons(h1, t1) =>
+        union(t1, insert1(in2, h1))
+      case Nil =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  //def union(in1: List, in2: List) = choose {
+  //  (out : List) =>
+  //    isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+  //}
+
+  def diff(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in2 match {
+      case Cons(h2, t2) =>
+        diff(delete(in1, h2), t2)
+      case Nil =>
+        in1
+    }
+  } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+  //def diff(in1: List, in2: List) = choose {
+  //  (out : List) =>
+  //    isSorted(in1) && isSorted(in2) && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+  //}
+
+  // ***********************
+  // Sorting algorithms
+  // ***********************
+
+  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) 
+  }
+
+  def abs(i : Int) : Int = {
+    if(i < 0) -i else i
+  } ensuring(_ >= 0)
+
+  def sortSpec(in : List, out : List) : Boolean = {
+    content(out) == content(in) && isSorted(out)
+  }
+
+
+  def split(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) = split(xs)
+      (Cons(x1, s1), Cons(x2, s2))
+  }) ensuring(res => splitSpec(list, res))
+
+  //def split(list : List) : (List,List) = {
+  //  choose { (res : (List,List)) => splitSpec(list, res) }
+  //}
+
+  def sort1(in : List) : List = (in match {
+    case Nil => Nil
+    case Cons(x, xs) => insert1(sort1(xs), x)
+  }) ensuring(res => sortSpec(in, res))
+
+  // Not really quicksort, neither mergesort.
+  def sort2(in : List) : List = (in match {
+    case Nil => Nil
+    case Cons(x, Nil) => Cons(x, Nil)
+    case _ =>
+      val (s1,s2) = split(in)
+      union(sort2(s1), sort2(s2))
+  }) ensuring(res => sortSpec(in, res))
+
+  //def sort(list: List): List = choose {
+  //  (res: List) => sortSpec(list, res)
+  //}
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Delete.scala b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
new file mode 100644
index 000000000..1b99aeb00
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
@@ -0,0 +1,80 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert1(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert1(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insert2(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          Cons(v, in1)
+        } else {
+          Cons(h, insert2(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
+
+  // def delete(in1: List, v: Int): List = {
+  //   require(isSorted(in1))
+  //   in1 match {
+  //     case Cons(h,t) =>
+  //       if (h < v) {
+  //         Cons(h, delete(t, v))
+  //       } else if (h == v) {
+  //         delete(t, v)
+  //       } else {
+  //         in1
+  //       }
+  //     case Nil =>
+  //       Nil
+  //   }
+  // } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  def delete(in1: List, v: Int) = choose {
+    (out : List) =>
+      isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Diff.scala b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
new file mode 100644
index 000000000..4dd0df64f
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
@@ -0,0 +1,101 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert1(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert1(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insert2(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          Cons(v, in1)
+        } else {
+          Cons(h, insert2(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          delete(t, v)
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  def union(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in1 match {
+      case Cons(h1, t1) =>
+        union(t1, insert1(in2, h1))
+      case Nil =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  // def diff(in1: List, in2: List): List = {
+  //   require(isSorted(in1) && isSorted(in2))
+  //   in2 match {
+  //     case Cons(h2, t2) =>
+  //       diff(delete(in1, h2), t2)
+  //     case Nil =>
+  //       in1
+  //   }
+  // } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+  def diff(in1: List, in2: List) = choose {
+    (out : List) =>
+      isSorted(in1) && isSorted(in2) && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+  }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert1.scala b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
new file mode 100644
index 000000000..1b9346640
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
@@ -0,0 +1,47 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert1(in1: List, v: Int): List = {
+  //   require(isSorted(in1))
+  //   in1 match {
+  //     case Cons(h, t) =>
+  //       if (v < h) {
+  //         Cons(v, in1)
+  //       } else if (v == h) {
+  //         in1
+  //       } else {
+  //         Cons(h, insert1(t, v))
+  //       }
+  //     case Nil =>
+  //       Cons(v, Nil)
+  //   }
+  // } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insert1(in1: List, v: Int) = choose {
+    (out : List) =>
+      isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+  }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert2.scala b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
new file mode 100644
index 000000000..98c7331e9
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
@@ -0,0 +1,47 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert2(in1: List, v: Int): List = {
+  //   require(isSorted(in1))
+  //   in1 match {
+  //     case Cons(h, t) =>
+  //       if (v < h) {
+  //         Cons(v, in1)
+  //       } else if (v == h) {
+  //         Cons(v, in1)
+  //       } else {
+  //         Cons(h, insert2(t, v))
+  //       }
+  //     case Nil =>
+  //       Cons(v, Nil)
+  //   }
+  // } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
+
+  def insert2(in1: List, v: Int) = choose {
+    (out : List) =>
+      isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+  }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Sort.scala b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
new file mode 100644
index 000000000..03619f39e
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
@@ -0,0 +1,142 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert1(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert1(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insert2(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          Cons(v, in1)
+        } else {
+          Cons(h, insert2(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          delete(t, v)
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  def union(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in1 match {
+      case Cons(h1, t1) =>
+        insert1(union(t1, in2), h1)
+      case Nil =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  def diff(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in2 match {
+      case Cons(h2, t2) =>
+        diff(delete(in1, h2), t2)
+      case Nil =>
+        in1
+    }
+  } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+  // ***********************
+  // Sorting algorithms
+  // ***********************
+
+  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) 
+  }
+
+  def abs(i : Int) : Int = {
+    if(i < 0) -i else i
+  } ensuring(_ >= 0)
+
+  def sortSpec(in : List, out : List) : Boolean = {
+    content(out) == content(in) && isSorted(out)
+  }
+
+
+  def split(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) = split(xs)
+      (Cons(x1, s1), Cons(x2, s2))
+  }) ensuring(res => splitSpec(list, res))
+
+  // def sort1(in : List) : List = (in match {
+  //   case Nil => Nil
+  //   case Cons(x, xs) => insert1(sort1(xs), x)
+  // }) ensuring(res => sortSpec(in, res))
+
+  // // Not really quicksort, neither mergesort.
+  // def sort2(in : List) : List = (in match {
+  //   case Nil => Nil
+  //   case Cons(x, Nil) => Cons(x, Nil)
+  //   case _ =>
+  //     val (s1,s2) = split(in)
+  //     union(sort2(s1), sort2(s2))
+  // }) ensuring(res => sortSpec(in, res))
+
+  def sort(list: List): List = choose {
+    (res: List) => sortSpec(list, res)
+  }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split.scala b/testcases/synthesis/oopsla2013/SortedList/Split.scala
new file mode 100644
index 000000000..5d28846ea
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Split.scala
@@ -0,0 +1,128 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert1(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert1(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insert2(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          Cons(v, in1)
+        } else {
+          Cons(h, insert2(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          delete(t, v)
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  def union(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in1 match {
+      case Cons(h1, t1) =>
+        union(t1, insert1(in2, h1))
+      case Nil =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  def diff(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in2 match {
+      case Cons(h2, t2) =>
+        diff(delete(in1, h2), t2)
+      case Nil =>
+        in1
+    }
+  } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+  // ***********************
+  // Sorting algorithms
+  // ***********************
+
+  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) 
+  }
+
+  def abs(i : Int) : Int = {
+    if(i < 0) -i else i
+  } ensuring(_ >= 0)
+
+  def sortSpec(in : List, out : List) : Boolean = {
+    content(out) == content(in) && isSorted(out)
+  }
+
+
+  // def split(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) = split(xs)
+  //     (Cons(x1, s1), Cons(x2, s2))
+  // }) ensuring(res => splitSpec(list, res))
+
+  def split(list : List) : (List,List) = {
+    choose { (res : (List,List)) => splitSpec(list, res) }
+  }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split1.scala b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
new file mode 100644
index 000000000..daa3b9deb
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
@@ -0,0 +1,128 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert1(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert1(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insert2(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          Cons(v, in1)
+        } else {
+          Cons(h, insert2(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          delete(t, v)
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  def union(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in1 match {
+      case Cons(h1, t1) =>
+        union(t1, insert1(in2, h1))
+      case Nil =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  def diff(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in2 match {
+      case Cons(h2, t2) =>
+        diff(delete(in1, h2), t2)
+      case Nil =>
+        in1
+    }
+  } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+  // ***********************
+  // Sorting algorithms
+  // ***********************
+
+  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) 
+  }
+
+  def abs(i : Int) : Int = {
+    if(i < 0) -i else i
+  } ensuring(_ >= 0)
+
+  def sortSpec(in : List, out : List) : Boolean = {
+    content(out) == content(in) && isSorted(out)
+  }
+
+
+  // def split(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) = split(xs)
+  //     (Cons(x1, s1), Cons(x2, s2))
+  // }) ensuring(res => splitSpec(list, res))
+
+  def split(list : List) : (List,List) = {
+    choose { (res : (List,List)) => (content(res._1) ++ content(res._2) == content(list)) }
+  }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split2.scala b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
new file mode 100644
index 000000000..fcdcf7b68
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
@@ -0,0 +1,128 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert1(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert1(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insert2(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          Cons(v, in1)
+        } else {
+          Cons(h, insert2(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          delete(t, v)
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  def union(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in1 match {
+      case Cons(h1, t1) =>
+        union(t1, insert1(in2, h1))
+      case Nil =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  def diff(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in2 match {
+      case Cons(h2, t2) =>
+        diff(delete(in1, h2), t2)
+      case Nil =>
+        in1
+    }
+  } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+  // ***********************
+  // Sorting algorithms
+  // ***********************
+
+  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) 
+  }
+
+  def abs(i : Int) : Int = {
+    if(i < 0) -i else i
+  } ensuring(_ >= 0)
+
+  def sortSpec(in : List, out : List) : Boolean = {
+    content(out) == content(in) && isSorted(out)
+  }
+
+
+  // def split(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) = split(xs)
+  //     (Cons(x1, s1), Cons(x2, s2))
+  // }) ensuring(res => splitSpec(list, res))
+
+  def split(list : List) : (List,List) = {
+    choose { (res : (List,List)) => (content(res._1) ++ content(res._2) == content(list)) && abs(size(res._1) - size(res._2)) <= 1 }
+  }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split3.scala b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
new file mode 100644
index 000000000..1042be56e
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
@@ -0,0 +1,128 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert1(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert1(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insert2(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          Cons(v, in1)
+        } else {
+          Cons(h, insert2(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          delete(t, v)
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  def union(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in1 match {
+      case Cons(h1, t1) =>
+        union(t1, insert1(in2, h1))
+      case Nil =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  def diff(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in2 match {
+      case Cons(h2, t2) =>
+        diff(delete(in1, h2), t2)
+      case Nil =>
+        in1
+    }
+  } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+  // ***********************
+  // Sorting algorithms
+  // ***********************
+
+  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) 
+  }
+
+  def abs(i : Int) : Int = {
+    if(i < 0) -i else i
+  } ensuring(_ >= 0)
+
+  def sortSpec(in : List, out : List) : Boolean = {
+    content(out) == content(in) && isSorted(out)
+  }
+
+
+  // def split(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) = split(xs)
+  //     (Cons(x1, s1), Cons(x2, s2))
+  // }) ensuring(res => splitSpec(list, res))
+
+  def split(list : List) : (List,List) = {
+    choose { (res : (List,List)) => (content(res._1) ++ content(res._2) == content(list)) && abs(size(res._1) - size(res._2)) <= 1 && (size(res._1) + size(res._2) == size(list)) }
+  }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Union.scala b/testcases/synthesis/oopsla2013/SortedList/Union.scala
new file mode 100644
index 000000000..394ca3a7a
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Union.scala
@@ -0,0 +1,91 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert1(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert1(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insert2(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          Cons(v, in1)
+        } else {
+          Cons(h, insert2(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          delete(t, v)
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  // def union(in1: List, in2: List): List = {
+  //   require(isSorted(in1) && isSorted(in2))
+  //   in1 match {
+  //     case Cons(h1, t1) =>
+  //       union(t1, insert1(in2, h1))
+  //     case Nil =>
+  //       in2
+  //   }
+  // } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  def union(in1: List, in2: List) = choose {
+    (out : List) =>
+      isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Complete.scala b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
new file mode 100644
index 000000000..21e2d277d
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
@@ -0,0 +1,114 @@
+import leon.Annotations._
+import leon.Utils._
+
+object SparseVector {
+  sealed abstract class SparseVector
+  case class  Cons(index: Int, value : Int, tail: SparseVector) extends SparseVector
+  case object Nil extends SparseVector
+
+  sealed abstract class Option
+  case class Some(v: Int) extends Option
+  case object None extends Option
+
+  def size(sv: SparseVector): Int = {
+    sv match {
+      case Cons(i, v, t) =>
+        1 + size(t)
+      case Nil =>
+        0
+    }
+  } ensuring { _ >= 0 }
+
+  def isDefined(o: Option) = o match {
+    case Some(v) => true
+    case None => false
+  }
+
+  def valueOf(o: Option) = o match {
+    case Some(v) => v
+    case None => -42
+  }
+
+  def values(sv: SparseVector): Set[Int] = sv match {
+    case Cons(i, v, t) =>
+      values(t) ++ Set(v)
+    case Nil =>
+      Set()
+  }
+
+  def indices(sv: SparseVector): Set[Int] = sv match {
+    case Cons(i, v, t) =>
+      indices(t) ++ Set(i)
+    case Nil =>
+      Set()
+  }
+
+  def invariant(sv: SparseVector): Boolean = sv match {
+    case Cons(i1, v1, t1 @ Cons(i2, v2, t2)) =>
+      (i1 < i2) && invariant(t1)
+    case _ => true
+  }
+
+  def set(sv: SparseVector, at: Int, newV: Int): SparseVector = {
+    require(invariant(sv))
+
+    sv match {
+      case Cons(i, v, t) =>
+        if (i == at) {
+          Cons(i, newV, t)
+        } else if (i > at) {
+          Cons(at, newV, sv)
+        } else {
+          Cons(i, v, set(t, at, newV))
+        }
+      case Nil =>
+        Cons(at, newV, Nil)
+    }
+  } ensuring { res => (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at)) }
+
+  //def set(sv: SparseVector, at: Int, newV: Int): SparseVector = choose {
+  //  (res: SparseVector) => invariant(sv) && (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at))
+  //}
+
+  def delete(sv: SparseVector, at: Int): SparseVector = {
+    require(invariant(sv))
+
+    sv match {
+      case Cons(i, v, t) =>
+        if (i == at) {
+          t
+        } else if (i > at) {
+          sv
+        } else {
+          Cons(i, v, delete(t, at))
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => (size(res) <= size(sv)) && invariant(res) && (indices(res) == indices(sv) -- Set(at)) }
+
+  //def delete(sv: SparseVector, at: Int): SparseVector = choose {
+  //  (res: SparseVector) => invariant(sv) && (size(res) <= size(sv)) && invariant(res) && (indices(res) == indices(sv) -- Set(at))
+  //}
+
+  def get(sv: SparseVector, at: Int): Option = {
+    require(invariant(sv))
+
+    sv match {
+      case Cons(i, v, t) =>
+        if (i == at) {
+          Some(v)
+        } else if (i > at) {
+          None
+        } else {
+          get(t, at)
+        }
+      case Nil =>
+        None
+    }
+  } ensuring { res => ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)) }
+
+  // def get(sv: SparseVector, at: Int): Option = choose {
+  //   (res: Option) => invariant(sv) && ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)))
+  // }
+}
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Delete.scala b/testcases/synthesis/oopsla2013/SparseVector/Delete.scala
new file mode 100644
index 000000000..9a9acedf2
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SparseVector/Delete.scala
@@ -0,0 +1,89 @@
+import leon.Annotations._
+import leon.Utils._
+
+object SparseVector {
+  sealed abstract class SparseVector
+  case class  Cons(index: Int, value : Int, tail: SparseVector) extends SparseVector
+  case object Nil extends SparseVector
+
+  sealed abstract class Option
+  case class Some(v: Int) extends Option
+  case object None extends Option
+
+  def size(sv: SparseVector): Int = {
+    sv match {
+      case Cons(i, v, t) =>
+        1 + size(t)
+      case Nil =>
+        0
+    }
+  } ensuring { _ >= 0 }
+
+  def isDefined(o: Option) = o match {
+    case Some(v) => true
+    case None => false
+  }
+
+  def valueOf(o: Option) = o match {
+    case Some(v) => v
+    case None => -42
+  }
+
+  def values(sv: SparseVector): Set[Int] = sv match {
+    case Cons(i, v, t) =>
+      values(t) ++ Set(v)
+    case Nil =>
+      Set()
+  }
+
+  def indices(sv: SparseVector): Set[Int] = sv match {
+    case Cons(i, v, t) =>
+      indices(t) ++ Set(i)
+    case Nil =>
+      Set()
+  }
+
+  def invariant(sv: SparseVector): Boolean = sv match {
+    case Cons(i1, v1, t1 @ Cons(i2, v2, t2)) =>
+      (i1 < i2) && invariant(t1)
+    case _ => true
+  }
+
+  def set(sv: SparseVector, at: Int, newV: Int): SparseVector = {
+    require(invariant(sv))
+
+    sv match {
+      case Cons(i, v, t) =>
+        if (i == at) {
+          Cons(i, newV, t)
+        } else if (i > at) {
+          Cons(at, newV, sv)
+        } else {
+          Cons(i, v, set(t, at, newV))
+        }
+      case Nil =>
+        Cons(at, newV, Nil)
+    }
+  } ensuring { res => (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at)) }
+
+  // def delete(sv: SparseVector, at: Int): SparseVector = {
+  //   require(invariant(sv))
+
+  //   sv match {
+  //     case Cons(i, v, t) =>
+  //       if (i == at) {
+  //         t
+  //       } else if (i > at) {
+  //         sv
+  //       } else {
+  //         Cons(i, v, delete(t, at))
+  //       }
+  //     case Nil =>
+  //       Nil
+  //   }
+  // } ensuring { res => (size(res) <= size(sv)) && invariant(res) && (indices(res) == indices(sv) -- Set(at)) }
+
+  def delete(sv: SparseVector, at: Int): SparseVector = choose {
+    (res: SparseVector) => invariant(sv) && (size(res) <= size(sv)) && invariant(res) && (indices(res) == indices(sv) -- Set(at))
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Get.scala b/testcases/synthesis/oopsla2013/SparseVector/Get.scala
new file mode 100644
index 000000000..1cf7a4cd2
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SparseVector/Get.scala
@@ -0,0 +1,106 @@
+import leon.Annotations._
+import leon.Utils._
+
+object SparseVector {
+  sealed abstract class SparseVector
+  case class  Cons(index: Int, value : Int, tail: SparseVector) extends SparseVector
+  case object Nil extends SparseVector
+
+  sealed abstract class Option
+  case class Some(v: Int) extends Option
+  case object None extends Option
+
+  def size(sv: SparseVector): Int = {
+    sv match {
+      case Cons(i, v, t) =>
+        1 + size(t)
+      case Nil =>
+        0
+    }
+  } ensuring { _ >= 0 }
+
+  def isDefined(o: Option) = o match {
+    case Some(v) => true
+    case None => false
+  }
+
+  def valueOf(o: Option) = o match {
+    case Some(v) => v
+    case None => -42
+  }
+
+  def values(sv: SparseVector): Set[Int] = sv match {
+    case Cons(i, v, t) =>
+      values(t) ++ Set(v)
+    case Nil =>
+      Set()
+  }
+
+  def indices(sv: SparseVector): Set[Int] = sv match {
+    case Cons(i, v, t) =>
+      indices(t) ++ Set(i)
+    case Nil =>
+      Set()
+  }
+
+  def invariant(sv: SparseVector): Boolean = sv match {
+    case Cons(i1, v1, t1 @ Cons(i2, v2, t2)) =>
+      (i1 < i2) && invariant(t1)
+    case _ => true
+  }
+
+  def set(sv: SparseVector, at: Int, newV: Int): SparseVector = {
+    require(invariant(sv))
+
+    sv match {
+      case Cons(i, v, t) =>
+        if (i == at) {
+          Cons(i, newV, t)
+        } else if (i > at) {
+          Cons(at, newV, sv)
+        } else {
+          Cons(i, v, set(t, at, newV))
+        }
+      case Nil =>
+        Cons(at, newV, Nil)
+    }
+  } ensuring { res => (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at)) }
+
+  def delete(sv: SparseVector, at: Int): SparseVector = {
+    require(invariant(sv))
+
+    sv match {
+      case Cons(i, v, t) =>
+        if (i == at) {
+          t
+        } else if (i > at) {
+          sv
+        } else {
+          Cons(i, v, delete(t, at))
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => (size(res) <= size(sv)) && invariant(res) && (indices(res) == indices(sv) -- Set(at)) }
+
+  // def get(sv: SparseVector, at: Int): Option = {
+  //   require(invariant(sv))
+
+  //   sv match {
+  //     case Cons(i, v, t) =>
+  //       if (i == at) {
+  //         Some(v)
+  //       } else if (i > at) {
+  //         None
+  //       } else {
+  //         get(t, at)
+  //       }
+  //     case Nil =>
+  //       None
+  //   }
+  // } ensuring { res => ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)) }
+
+  def get(sv: SparseVector, at: Int): Option = choose {
+    (res: Option) => invariant(sv) && ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)))
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Set.scala b/testcases/synthesis/oopsla2013/SparseVector/Set.scala
new file mode 100644
index 000000000..f36589c39
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SparseVector/Set.scala
@@ -0,0 +1,72 @@
+import leon.Annotations._
+import leon.Utils._
+
+object SparseVector {
+  sealed abstract class SparseVector
+  case class  Cons(index: Int, value : Int, tail: SparseVector) extends SparseVector
+  case object Nil extends SparseVector
+
+  sealed abstract class Option
+  case class Some(v: Int) extends Option
+  case object None extends Option
+
+  def size(sv: SparseVector): Int = {
+    sv match {
+      case Cons(i, v, t) =>
+        1 + size(t)
+      case Nil =>
+        0
+    }
+  } ensuring { _ >= 0 }
+
+  def isDefined(o: Option) = o match {
+    case Some(v) => true
+    case None => false
+  }
+
+  def valueOf(o: Option) = o match {
+    case Some(v) => v
+    case None => -42
+  }
+
+  def values(sv: SparseVector): Set[Int] = sv match {
+    case Cons(i, v, t) =>
+      values(t) ++ Set(v)
+    case Nil =>
+      Set()
+  }
+
+  def indices(sv: SparseVector): Set[Int] = sv match {
+    case Cons(i, v, t) =>
+      indices(t) ++ Set(i)
+    case Nil =>
+      Set()
+  }
+
+  def invariant(sv: SparseVector): Boolean = sv match {
+    case Cons(i1, v1, t1 @ Cons(i2, v2, t2)) =>
+      (i1 < i2) && invariant(t1)
+    case _ => true
+  }
+
+  // def set(sv: SparseVector, at: Int, newV: Int): SparseVector = {
+  //   require(invariant(sv))
+
+  //   sv match {
+  //     case Cons(i, v, t) =>
+  //       if (i == at) {
+  //         Cons(i, newV, t)
+  //       } else if (i > at) {
+  //         Cons(at, newV, sv)
+  //       } else {
+  //         Cons(i, v, set(t, at, newV))
+  //       }
+  //     case Nil =>
+  //       Cons(at, newV, Nil)
+  //   }
+  // } ensuring { res => (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at)) }
+
+  def set(sv: SparseVector, at: Int, newV: Int): SparseVector = choose {
+    (res: SparseVector) => invariant(sv) && (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at))
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
new file mode 100644
index 000000000..c4a8096de
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
@@ -0,0 +1,99 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  //def insert1(in1: List, v: Int) = choose {
+  //  (out : List) =>
+  //    isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+  //}
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          t
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  //def delete(in1: List, v: Int) = choose {
+  //  (out : List) =>
+  //    isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+  //}
+
+  def union(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in1 match {
+      case Cons(h1, t1) =>
+        union(t1, insert(in2, h1))
+      case Nil =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  //def union(in1: List, in2: List) = choose {
+  //  (out : List) =>
+  //    isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+  //}
+
+  def diff(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in2 match {
+      case Cons(h2, t2) =>
+        diff(delete(in1, h2), t2)
+      case Nil =>
+        in1
+    }
+  } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+  //def diff(in1: List, in2: List) = choose {
+  //  (out : List) =>
+  //    isSorted(in1) && isSorted(in2) && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+  //}
+
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
new file mode 100644
index 000000000..a0b56fa9d
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
@@ -0,0 +1,63 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Delete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  // def delete(in1: List, v: Int): List = {
+  //   require(isSorted(in1))
+  //   in1 match {
+  //     case Cons(h,t) =>
+  //       if (h < v) {
+  //         Cons(h, delete(t, v))
+  //       } else if (h == v) {
+  //         t
+  //       } else {
+  //         in1
+  //       }
+  //     case Nil =>
+  //       Nil
+  //   }
+  // } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  def delete(in1: List, v: Int) = choose {
+    (out : List) =>
+      isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+  }
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
new file mode 100644
index 000000000..eea2a1eac
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
@@ -0,0 +1,84 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          t
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  def union(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    in1 match {
+      case Cons(h1, t1) =>
+        union(t1, insert(in2, h1))
+      case Nil =>
+        in2
+    }
+  } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  // def diff(in1: List, in2: List): List = {
+  //   require(isSorted(in1) && isSorted(in2))
+  //   in2 match {
+  //     case Cons(h2, t2) =>
+  //       diff(delete(in1, h2), t2)
+  //     case Nil =>
+  //       in1
+  //   }
+  // } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+  def diff(in1: List, in2: List) = choose {
+    (out : List) =>
+      isSorted(in1) && isSorted(in2) && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+  }
+
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
new file mode 100644
index 000000000..31344aec3
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
@@ -0,0 +1,47 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert(in1: List, v: Int): List = {
+  //   require(isSorted(in1))
+  //   in1 match {
+  //     case Cons(h, t) =>
+  //       if (v < h) {
+  //         Cons(v, in1)
+  //       } else if (v == h) {
+  //         in1
+  //       } else {
+  //         Cons(h, insert(t, v))
+  //       }
+  //     case Nil =>
+  //       Cons(v, Nil)
+  //   }
+  // } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def insert(in1: List, v: Int) = choose {
+    (out : List) =>
+      isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+  }
+
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
new file mode 100644
index 000000000..e44158330
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
@@ -0,0 +1,73 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : Int = (l match {
+      case Nil => 0
+      case Cons(_, t) => 1 + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[Int] = l match {
+    case Nil => Set.empty[Int]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 insert(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h, t) =>
+        if (v < h) {
+          Cons(v, in1)
+        } else if (v == h) {
+          in1
+        } else {
+          Cons(h, insert(t, v))
+        }
+      case Nil =>
+        Cons(v, Nil)
+    }
+
+  } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+  def delete(in1: List, v: Int): List = {
+    require(isSorted(in1))
+    in1 match {
+      case Cons(h,t) =>
+        if (h < v) {
+          Cons(h, delete(t, v))
+        } else if (h == v) {
+          t
+        } else {
+          in1
+        }
+      case Nil =>
+        Nil
+    }
+  } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+  //def union(in1: List, in2: List): List = {
+  //  require(isSorted(in1) && isSorted(in2))
+  //  in1 match {
+  //    case Cons(h1, t1) =>
+  //      union(t1, insert(in2, h1))
+  //    case Nil =>
+  //      in2
+  //  }
+  //} ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+  def union(in1: List, in2: List) = choose {
+    (out : List) =>
+      isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+  }
+}
-- 
GitLab