diff --git a/testcases/synthesis/PrimeHeuristic.scala.off b/testcases/synthesis/PrimeHeuristic.scala.off
deleted file mode 100644
index 31a68993597650b3c4c6242a53150456e8a34bd9..0000000000000000000000000000000000000000
--- a/testcases/synthesis/PrimeHeuristic.scala.off
+++ /dev/null
@@ -1,11 +0,0 @@
-import leon.lang._
-
-object PrimeHeuristic {
-  def maybePrime(n: Int): Boolean = n match {
-      case 2 * k     => false
-      case 3 * k     => false
-      case 6 * k - 1 => true
-      case 6 * k + 1 => true
-  }
-
-}
diff --git a/testcases/synthesis/ADTInduction.scala b/testcases/synthesis/archives/ADTInduction.scala
similarity index 100%
rename from testcases/synthesis/ADTInduction.scala
rename to testcases/synthesis/archives/ADTInduction.scala
diff --git a/testcases/synthesis/BinaryTree.scala b/testcases/synthesis/archives/BinaryTree.scala
similarity index 100%
rename from testcases/synthesis/BinaryTree.scala
rename to testcases/synthesis/archives/BinaryTree.scala
diff --git a/testcases/synthesis/CegisExamples.scala b/testcases/synthesis/archives/CegisExamples.scala
similarity index 100%
rename from testcases/synthesis/CegisExamples.scala
rename to testcases/synthesis/archives/CegisExamples.scala
diff --git a/testcases/synthesis/CegisFunctions.scala b/testcases/synthesis/archives/CegisFunctions.scala
similarity index 100%
rename from testcases/synthesis/CegisFunctions.scala
rename to testcases/synthesis/archives/CegisFunctions.scala
diff --git a/testcases/synthesis/ChooseArith.scala b/testcases/synthesis/archives/ChooseArith.scala
similarity index 100%
rename from testcases/synthesis/ChooseArith.scala
rename to testcases/synthesis/archives/ChooseArith.scala
diff --git a/testcases/synthesis/ChooseIneq.scala b/testcases/synthesis/archives/ChooseIneq.scala
similarity index 100%
rename from testcases/synthesis/ChooseIneq.scala
rename to testcases/synthesis/archives/ChooseIneq.scala
diff --git a/testcases/synthesis/ChoosePos.scala b/testcases/synthesis/archives/ChoosePos.scala
similarity index 100%
rename from testcases/synthesis/ChoosePos.scala
rename to testcases/synthesis/archives/ChoosePos.scala
diff --git a/testcases/synthesis/ChurchNumerals.scala b/testcases/synthesis/archives/ChurchNumerals.scala
similarity index 100%
rename from testcases/synthesis/ChurchNumerals.scala
rename to testcases/synthesis/archives/ChurchNumerals.scala
diff --git a/testcases/synthesis/DrSuter.scala b/testcases/synthesis/archives/DrSuter.scala
similarity index 100%
rename from testcases/synthesis/DrSuter.scala
rename to testcases/synthesis/archives/DrSuter.scala
diff --git a/testcases/synthesis/FastExp.scala b/testcases/synthesis/archives/FastExp.scala
similarity index 100%
rename from testcases/synthesis/FastExp.scala
rename to testcases/synthesis/archives/FastExp.scala
diff --git a/testcases/synthesis/FiniteSort.scala b/testcases/synthesis/archives/FiniteSort.scala
similarity index 100%
rename from testcases/synthesis/FiniteSort.scala
rename to testcases/synthesis/archives/FiniteSort.scala
diff --git a/testcases/synthesis/Injection.scala b/testcases/synthesis/archives/Injection.scala
similarity index 100%
rename from testcases/synthesis/Injection.scala
rename to testcases/synthesis/archives/Injection.scala
diff --git a/testcases/synthesis/InnerSplit.scala b/testcases/synthesis/archives/InnerSplit.scala
similarity index 100%
rename from testcases/synthesis/InnerSplit.scala
rename to testcases/synthesis/archives/InnerSplit.scala
diff --git a/testcases/synthesis/Justify.scala b/testcases/synthesis/archives/Justify.scala
similarity index 100%
rename from testcases/synthesis/Justify.scala
rename to testcases/synthesis/archives/Justify.scala
diff --git a/testcases/synthesis/Matching.scala b/testcases/synthesis/archives/Matching.scala
similarity index 100%
rename from testcases/synthesis/Matching.scala
rename to testcases/synthesis/archives/Matching.scala
diff --git a/testcases/synthesis/ScaleWeight.scala b/testcases/synthesis/archives/ScaleWeight.scala
similarity index 100%
rename from testcases/synthesis/ScaleWeight.scala
rename to testcases/synthesis/archives/ScaleWeight.scala
diff --git a/testcases/synthesis/Sec2Time.scala b/testcases/synthesis/archives/Sec2Time.scala
similarity index 100%
rename from testcases/synthesis/Sec2Time.scala
rename to testcases/synthesis/archives/Sec2Time.scala
diff --git a/testcases/synthesis/SimplestCegis.scala b/testcases/synthesis/archives/SimplestCegis.scala
similarity index 100%
rename from testcases/synthesis/SimplestCegis.scala
rename to testcases/synthesis/archives/SimplestCegis.scala
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/archives/Spt.scala
similarity index 100%
rename from testcases/synthesis/Spt.scala
rename to testcases/synthesis/archives/Spt.scala
diff --git a/testcases/synthesis/Unification.scala b/testcases/synthesis/archives/Unification.scala
similarity index 100%
rename from testcases/synthesis/Unification.scala
rename to testcases/synthesis/archives/Unification.scala
diff --git a/testcases/synthesis/ZuneBug.scala b/testcases/synthesis/archives/ZuneBug.scala
similarity index 100%
rename from testcases/synthesis/ZuneBug.scala
rename to testcases/synthesis/archives/ZuneBug.scala
diff --git a/testcases/synthesis/current/AddressBook/Make.scala b/testcases/synthesis/current/AddressBook/Make.scala
new file mode 100644
index 0000000000000000000000000000000000000000..612effe382140cfc87bd0c12d791c4de9ddfae8e
--- /dev/null
+++ b/testcases/synthesis/current/AddressBook/Make.scala
@@ -0,0 +1,66 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object AddressBookMake {
+
+  case class Address[A](info: A, priv: Boolean)
+
+  sealed abstract class AddressList[A] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(head, tail) => BigInt(1) + tail.size
+      }
+    } ensuring { res => res >= 0 }
+
+    def content: Set[Address[A]] = this match {
+      case Nil() => Set[Address[A]]()
+      case Cons(addr, l1) => Set(addr) ++ l1.content
+    }
+  }
+
+  case class Cons[A](a: Address[A], tail: AddressList[A]) extends AddressList[A]
+  case class Nil[A]() extends AddressList[A]
+
+  def allPersonal[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) allPersonal(l1)
+      else false
+  }
+
+  def allBusiness[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) false
+      else allBusiness(l1)
+  }
+
+  case class AddressBook[A](business: AddressList[A], personal: AddressList[A]) {
+    def size: BigInt = business.size + personal.size
+
+    def content: Set[Address[A]] = business.content ++ personal.content
+
+    def invariant = {
+      allPersonal(personal) && allBusiness(business)
+    }
+  }
+
+  def makeAddressBook[A](as: AddressList[A]): AddressBook[A] = {
+    choose( (res: AddressBook[A]) => res.content == as.content && res.invariant )
+
+ /*   as match {
+      case Nil() => AddressBook[A](Nil[A](), Nil[A]())
+      case Cons(x, xs) =>
+        val AddressBook(b, p) = makeAddressBook(xs)
+        if(x.priv) AddressBook(b, Cons(x, p))
+        else AddressBook(Cons(x, b), p)
+    }
+
+  } ensuring { 
+    res => res.content == as.content && res.invariant */
+  }
+
+
+}
diff --git a/testcases/synthesis/current/AddressBook/Merge.scala b/testcases/synthesis/current/AddressBook/Merge.scala
new file mode 100644
index 0000000000000000000000000000000000000000..92a5b5bfef213e35c4f2a76bbbc9f295e406d1f4
--- /dev/null
+++ b/testcases/synthesis/current/AddressBook/Merge.scala
@@ -0,0 +1,69 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object AddressBookMake {
+
+  case class Address[A](info: A, priv: Boolean)
+
+  sealed abstract class AddressList[A] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(head, tail) => BigInt(1) + tail.size
+      }
+    } ensuring { res => res >= 0 }
+
+    def content: Set[Address[A]] = this match {
+      case Nil() => Set[Address[A]]()
+      case Cons(addr, l1) => Set(addr) ++ l1.content
+    }
+
+    def ++(that: AddressList[A]): AddressList[A] = {
+      this match {
+        case Cons(h, t) => Cons(h, t ++ that)
+        case Nil() => that
+      }
+    } ensuring {
+      res => res.content == this.content ++ that.content
+    }
+  }
+
+  case class Cons[A](a: Address[A], tail: AddressList[A]) extends AddressList[A]
+  case class Nil[A]() extends AddressList[A]
+
+  def allPersonal[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) allPersonal(l1)
+      else false
+  }
+
+  def allBusiness[A](l: AddressList[A]): Boolean = l match {
+    case Nil() => true
+    case Cons(a, l1) =>
+      if (a.priv) false
+      else allBusiness(l1)
+  }
+
+  case class AddressBook[A](business: AddressList[A], personal: AddressList[A]) {
+    def size: BigInt = business.size + personal.size
+
+    def content: Set[Address[A]] = business.content ++ personal.content
+
+    @inline
+    def invariant = {
+      allPersonal(personal) && allBusiness(business)
+    }
+  }
+
+  def merge[A](a1: AddressBook[A], a2: AddressBook[A]): AddressBook[A] = {
+    require(a1.invariant && a2.invariant)
+
+    choose( (res: AddressBook[A]) =>
+      res.personal.content == (a1.personal.content ++ a2.personal.content) &&
+      res.business.content == (a1.business.content ++ a2.business.content) &&
+      res.invariant
+    )
+  }
+}
diff --git a/testcases/synthesis/current/BatchedQueue/Dequeue.scala b/testcases/synthesis/current/BatchedQueue/Dequeue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c44fc062847b9af2264a9b3bba05186a313ab36b
--- /dev/null
+++ b/testcases/synthesis/current/BatchedQueue/Dequeue.scala
@@ -0,0 +1,80 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object BatchedQueue {
+  sealed abstract class List[T] {
+    def content: Set[T] = {
+      this match {
+        case Cons(h, t) => Set(h) ++ t.content
+        case Nil() => Set()
+      }
+    }
+
+    def size: BigInt = {
+      this match {
+        case Cons(h, t) => BigInt(1) + t.size
+        case Nil() => BigInt(0)
+      }
+    } ensuring { _ >= 0 }
+
+    def reverse: List[T] = {
+      this match {
+        case Cons(h, t) => t.reverse.append(Cons(h, Nil[T]()))
+        case Nil() => Nil[T]()
+      }
+    } ensuring { res =>
+      this.content == res.content
+    }
+
+    def append(r: List[T]): List[T] = {
+      this match {
+        case Cons(h, t) => Cons(h, t.append(r))
+        case Nil() => r
+      }
+    }
+
+    def isEmpty: Boolean = {
+      this == Nil[T]()
+    }
+
+    def tail: List[T] = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => t
+      }
+    }
+
+    def head: T = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => h
+      }
+    }
+  }
+
+  case class Cons[T](h: T, t: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+  case class Queue[T](f: List[T], r: List[T]) {
+    def content: Set[T] = f.content ++ r.content
+    def size: BigInt = f.size + r.size
+
+    def isEmpty: Boolean = f.isEmpty && r.isEmpty
+
+    def invariant: Boolean = {
+      (f.isEmpty) ==> (r.isEmpty)
+    }
+
+    def toList: List[T] = f.append(r.reverse)
+
+    def dequeue: Queue[T] = {
+      require(invariant && !isEmpty)
+
+      choose { (res: Queue[T]) =>
+        res.size == size-1 && res.toList == this.toList.tail && res.invariant
+      }
+    }
+  }
+
+  val test = Queue[BigInt](Cons(42, Nil()), Nil()).dequeue
+}
diff --git a/testcases/synthesis/current/BatchedQueue/Enqueue.scala b/testcases/synthesis/current/BatchedQueue/Enqueue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0f30a5ba1a95d39e78a1594f39804c8161e919a6
--- /dev/null
+++ b/testcases/synthesis/current/BatchedQueue/Enqueue.scala
@@ -0,0 +1,83 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object BatchedQueue {
+  sealed abstract class List[T] {
+    def content: Set[T] = {
+      this match {
+        case Cons(h, t) => Set(h) ++ t.content
+        case Nil() => Set()
+      }
+    }
+
+    def size: BigInt = {
+      this match {
+        case Cons(h, t) => BigInt(1) + t.size
+        case Nil() => BigInt(0)
+      }
+    } ensuring { _ >= 0 }
+
+    def reverse: List[T] = {
+      this match {
+        case Cons(h, t) => t.reverse.append(Cons(h, Nil[T]()))
+        case Nil() => Nil[T]()
+      }
+    } ensuring { res =>
+      this.content == res.content
+    }
+
+    def append(r: List[T]): List[T] = {
+      this match {
+        case Cons(h, t) => Cons(h, t.append(r))
+        case Nil() => r
+      }
+    }
+
+    def tail: List[T] = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => t
+      }
+    }
+
+    def head: T = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, t) => h
+      }
+    }
+
+    def last: T = {
+      require(this != Nil[T]())
+      this match {
+        case Cons(h, Nil()) => h
+        case Cons(h, t) => t.last
+      }
+    }
+  }
+
+  case class Cons[T](h: T, t: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+  case class Queue[T](f: List[T], r: List[T]) {
+    def content: Set[T] = f.content ++ r.content
+    def size: BigInt = f.size + r.size
+
+    def invariant: Boolean = {
+      (f == Nil[T]()) ==> (r == Nil[T]())
+    }
+
+    def toList: List[T] = f.append(r.reverse)
+
+    def enqueue(v: T): Queue[T] = {
+      require(invariant)
+
+      ???[Queue[T]]
+    } ensuring { (res: Queue[T]) =>
+      res.invariant &&
+      res.toList.last == v &&
+      res.size == size + 1 &&
+      res.content == this.content ++ Set(v)
+    }
+  }
+}
diff --git a/testcases/synthesis/current/Compiler/Desugar.scala b/testcases/synthesis/current/Compiler/Desugar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2684c71b2b8bbc9e5fe6cc307899ca7b92d366b4
--- /dev/null
+++ b/testcases/synthesis/current/Compiler/Desugar.scala
@@ -0,0 +1,118 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(lhs: Expr, rhs: Expr) extends Expr
+  case class Or(lhs: Expr, rhs: Expr) extends Expr
+  case class Not(e : Expr) extends Expr
+  case class Eq(lhs: Expr, rhs: Expr) extends Expr
+  case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+  case class BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+  def rewriteMinus(in: Minus): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Minus])
+    }
+  }
+
+  def rewriteImplies(in: Implies): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Implies])
+    }
+  }
+
+
+  def plop(x: Expr) = {
+    eval(x) == Error//eval(Not(IntLiteral(BigInt(2))))
+  }.holds
+}
diff --git a/testcases/synthesis/current/Compiler/DesugarImplies.scala b/testcases/synthesis/current/Compiler/DesugarImplies.scala
new file mode 100644
index 0000000000000000000000000000000000000000..de5c544ff368043ca7847376af8cd9ae6b513f4d
--- /dev/null
+++ b/testcases/synthesis/current/Compiler/DesugarImplies.scala
@@ -0,0 +1,144 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(lhs: Expr, rhs: Expr) extends Expr
+  case class Or(lhs: Expr, rhs: Expr) extends Expr
+  case class Not(e : Expr) extends Expr
+  case class Eq(lhs: Expr, rhs: Expr) extends Expr
+  case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+  case class BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  def exists(e: Expr, f: Expr => Boolean): Boolean = {
+    f(e) || (e match {
+      case Plus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Minus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case LessThan(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Eq(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Ite(c, t, e) => exists(c, f) || exists(t, f) || exists(e, f)
+      case Not(e) => exists(e, f)
+      case UMinus(e) => exists(e, f)
+      case _ => false
+    })
+  }
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+
+  //def desugar(e: Expr): Expr = {
+  //  choose{ (out: Expr) =>
+  //    eval(e) == eval(out) && !exists(out, f => f.isInstanceOf[Implies])
+  //  }
+  //}
+
+  def desugar(e: Expr): Expr = {
+    e match {
+      case Plus(lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+      case Minus(lhs, rhs) => Minus(desugar(lhs), desugar(rhs))
+      case LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+      case And(lhs, rhs) => And(desugar(lhs), desugar(rhs))
+      case Or(lhs, rhs) => Or(desugar(lhs), desugar(rhs))
+      case Implies(lhs, rhs) => //Implies(desugar(lhs), desugar(rhs))
+        Or(Not(desugar(lhs)), desugar(rhs))
+      case Eq(lhs, rhs) => Eq(desugar(lhs), desugar(rhs))
+      case Ite(c, t, e) => Ite(desugar(c), desugar(t), desugar(e))
+      case Not(e) => Not(desugar(e))
+      case UMinus(e) => UMinus(desugar(e))
+      case e => e
+    }
+  } ensuring { out =>
+    //eval(e) == eval(out) && 
+    !exists(out, f => f.isInstanceOf[Implies])
+  }
+}
diff --git a/testcases/synthesis/current/Compiler/RewriteImplies.scala b/testcases/synthesis/current/Compiler/RewriteImplies.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4b50b9cbe34043f65d1a8feeaadac929822e6c70
--- /dev/null
+++ b/testcases/synthesis/current/Compiler/RewriteImplies.scala
@@ -0,0 +1,124 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(lhs: Expr, rhs: Expr) extends Expr
+  case class Or(lhs: Expr, rhs: Expr) extends Expr
+  case class Not(e : Expr) extends Expr
+  case class Eq(lhs: Expr, rhs: Expr) extends Expr
+  case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+  case class BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  def exists(e: Expr, f: Expr => Boolean): Boolean = {
+    f(e) || (e match {
+      case Plus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Minus(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case LessThan(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case And(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Or(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Implies(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Eq(lhs, rhs) => exists(lhs, f) || exists(rhs, f)
+      case Ite(c, t, e) => exists(c, f) || exists(t, f) || exists(e, f)
+      case Not(e) => exists(e, f)
+      case UMinus(e) => exists(e, f)
+      case _ => false
+    })
+  }
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+
+  def desugar(in: Expr): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Implies])
+    }
+  }
+}
diff --git a/testcases/synthesis/current/Compiler/RewriteMinus.scala b/testcases/synthesis/current/Compiler/RewriteMinus.scala
new file mode 100644
index 0000000000000000000000000000000000000000..de2fa4360de5fa899110b43c171e592be5282803
--- /dev/null
+++ b/testcases/synthesis/current/Compiler/RewriteMinus.scala
@@ -0,0 +1,107 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon._
+
+object Compiler {
+  abstract class Expr
+  case class Plus(lhs: Expr, rhs: Expr) extends Expr
+  case class Minus(lhs: Expr, rhs: Expr) extends Expr
+  case class UMinus(e: Expr) extends Expr
+  case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+  case class And(lhs: Expr, rhs: Expr) extends Expr
+  case class Implies(lhs: Expr, rhs: Expr) extends Expr
+  case class Or(lhs: Expr, rhs: Expr) extends Expr
+  case class Not(e : Expr) extends Expr
+  case class Eq(lhs: Expr, rhs: Expr) extends Expr
+  case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+  case class BoolLiteral(b : Boolean) extends Expr
+  case class IntLiteral(i: BigInt) extends Expr
+
+  abstract class Value
+  case class BoolValue(b: Boolean) extends Value
+  case class IntValue(i: BigInt) extends Value
+  case object Error extends Value
+
+  def eval(e: Expr): Value = e match {
+    case Plus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il+ir)
+        case _ => Error
+      }
+
+    case Minus(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => IntValue(il-ir)
+        case _ => Error
+      }
+
+    case UMinus(l) =>
+      eval(l) match {
+        case IntValue(b) => IntValue(-b)
+        case _ => Error
+      }
+
+    case LessThan(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir)) => BoolValue(il < ir)
+        case _ => Error
+      }
+
+    case And(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(false) => b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Or(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          b
+        case b: BoolValue =>
+          eval(r)
+        case _ =>
+          Error
+      }
+
+    case Implies(l, r) =>
+      eval(l) match {
+        case b @ BoolValue(true) =>
+          eval(r)
+        case b @ BoolValue(false) =>
+          BoolValue(true)
+        case _ => Error
+      }
+
+    case Not(l) =>
+      eval(l) match {
+        case BoolValue(b) => BoolValue(!b)
+        case _ => Error
+      }
+
+    case Eq(l, r) =>
+      (eval(l), eval(r)) match {
+        case (IntValue(il), IntValue(ir))   => BoolValue(il == ir)
+        case (BoolValue(il), BoolValue(ir)) => BoolValue(il == ir)
+        case _ => Error
+      }
+
+    case Ite(c, t, e) =>
+      eval(c) match {
+        case BoolValue(true) => eval(t)
+        case BoolValue(false) => eval(t)
+        case _ => Error
+      }
+
+    case IntLiteral(l)  => IntValue(l)
+    case BoolLiteral(b) => BoolValue(b)
+  }
+
+  def rewriteMinus(in: Minus): Expr = {
+    choose{ (out: Expr) =>
+      eval(in) == eval(out) && !(out.isInstanceOf[Minus])
+    }
+  }
+}
diff --git a/testcases/synthesis/current/List/Delete.scala b/testcases/synthesis/current/List/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..30716c5919256f052d0a0e741a147d30c5bc82fa
--- /dev/null
+++ b/testcases/synthesis/current/List/Delete.scala
@@ -0,0 +1,26 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Delete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def delete(in: List, v: BigInt) = {
+    ???[List]
+  } ensuring {
+    (out : List) =>
+      content(out) == content(in) -- Set(v)
+  }
+}
diff --git a/testcases/synthesis/current/List/Diff.scala b/testcases/synthesis/current/List/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9fb3ade9558a7db175c6056efb9bf724f487d7ca
--- /dev/null
+++ b/testcases/synthesis/current/List/Diff.scala
@@ -0,0 +1,50 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Diff {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    Cons(v, in1)
+  } ensuring { content(_) == content(in1) ++ Set(v) }
+
+  def delete(in1: List, v: BigInt): 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 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/current/List/IndexOfInt.scala b/testcases/synthesis/current/List/IndexOfInt.scala
new file mode 100644
index 0000000000000000000000000000000000000000..595d40cf3ca361506ab2efccc19a0fa1140d9429
--- /dev/null
+++ b/testcases/synthesis/current/List/IndexOfInt.scala
@@ -0,0 +1,67 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object IndexOf {
+  sealed abstract class List[T] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(_, t) => BigInt(1) + t.size
+      }
+    } ensuring {
+      res => res >= 0
+    }
+
+    def content: Set[T] = this match {
+      case Nil() => Set.empty[T]
+      case Cons(i, t) => Set(i) ++ t.content
+    }
+
+    def apply(i: BigInt): T = {
+      require(i >= 0 && i < size)
+      this match {
+        case Cons(h, t) =>
+          if (i == 0) {
+            h
+          } else {
+            t.apply(i-1)
+          }
+      }
+    } ensuring { e =>
+      content contains e
+    }
+
+    def indexOfInt(e: T): BigInt = {
+      ???[BigInt]
+      
+      //this match {
+      //  case Cons(h, t) =>
+      //    val r = t.indexOfInt(e)
+
+      //    if (e == h) {
+      //      BigInt(0)
+      //    } else {
+      //      if (r < 0) {
+      //        r
+      //      } else {
+      //        r + 1
+      //      }
+      //    }
+      //  case Nil() =>
+      //    BigInt(-1)
+      //}
+      
+    } ensuring { res =>
+      if (res < 0) {
+        !(content contains e)
+      } else {
+        res < size && apply(res) == e
+      }
+    }
+  }
+
+  case class Cons[T](head: T, tail: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+}
diff --git a/testcases/synthesis/current/List/IndexOfOpt.scala b/testcases/synthesis/current/List/IndexOfOpt.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6738e5c23ff8764209bd43538c1e841fd894756e
--- /dev/null
+++ b/testcases/synthesis/current/List/IndexOfOpt.scala
@@ -0,0 +1,65 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object IndexOf {
+  sealed abstract class List[T] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(_, t) => BigInt(1) + t.size
+      }
+    } ensuring {
+      res => res >= 0
+    }
+
+    def content: Set[T] = this match {
+      case Nil() => Set.empty[T]
+      case Cons(i, t) => Set(i) ++ t.content
+    }
+
+    def apply(i: BigInt): T = {
+      require(i >= 0 && i < size)
+      this match {
+        case Cons(h, t) =>
+          if (i == 0) {
+            h
+          } else {
+            t.apply(i-1)
+          }
+      }
+    } ensuring { e =>
+      content contains e
+    }
+
+    def indexOfOpt(e: T): Option[BigInt] = {
+      ???[Option[BigInt]]
+      /*
+      this match {
+        case Cons(h, t) =>
+          val r = t.indexOfOpt(e)
+
+          if (e == h) {
+            Some(BigInt(0))
+          } else {
+            r match {
+              case Some(i) => Some(i+1)
+              case None() => None[BigInt]()
+            }
+          }
+        case Nil() =>
+          None[BigInt]()
+      }
+      */
+    } ensuring { res =>
+      res match {
+        case None() => !(content contains e)
+        case Some(i) => i >= 0 && i < size && apply(i) == e
+      }
+    }
+  }
+
+  case class Cons[T](head: T, tail: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+}
diff --git a/testcases/synthesis/current/List/IndexOfOpt2.scala b/testcases/synthesis/current/List/IndexOfOpt2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ff85f7a1c42e067b2266a948027dd22445bedca5
--- /dev/null
+++ b/testcases/synthesis/current/List/IndexOfOpt2.scala
@@ -0,0 +1,67 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object IndexOf {
+  sealed abstract class List[T] {
+    def size: BigInt = {
+      this match {
+        case Nil() => BigInt(0)
+        case Cons(_, t) => BigInt(1) + t.size
+      }
+    } ensuring {
+      res => res >= 0
+    }
+
+    def content: Set[T] = this match {
+      case Nil() => Set.empty[T]
+      case Cons(i, t) => Set(i) ++ t.content
+    }
+
+    def apply(i: BigInt): T = {
+      require(i >= 0 && i < size)
+      this match {
+        case Cons(h, t) =>
+          if (i == 0) {
+            h
+          } else {
+            t.apply(i-1)
+          }
+      }
+    } ensuring { e =>
+      content contains e
+    }
+
+    def indexOfOpt(e: T, offset: BigInt): Option[BigInt] = {
+      ???[Option[BigInt]]
+      /*
+      this match {
+        case Cons(h, t) =>
+          val r = t.indexOfOpt(e)
+
+          if (e == h) {
+            Some(BigInt(0))
+          } else {
+            r match {
+              case Some(i) => Some(i+1)
+              case None() => None[BigInt]()
+            }
+          }
+        case Nil() =>
+          None[BigInt]()
+      }
+      */
+    } ensuring { res =>
+      res match {
+        case None() => !(content contains e)
+        case Some(r) =>
+          val i = r - offset;
+          i >= 0 && i < size && apply(i) == e
+      }
+    }
+  }
+
+  case class Cons[T](head: T, tail: List[T]) extends List[T]
+  case class Nil[T]() extends List[T]
+
+}
diff --git a/testcases/synthesis/current/List/Insert.scala b/testcases/synthesis/current/List/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..48c38f4df0098410814f3ed27038c9c36c0d6532
--- /dev/null
+++ b/testcases/synthesis/current/List/Insert.scala
@@ -0,0 +1,28 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Insert {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  //def insert(in1: List, v: BigInt): List = {
+  //  Cons(v, in1)
+  //} ensuring { content(_) == content(in1) ++ Set(v) }
+
+  def insert(in1: List, v: BigInt) = choose {
+    (out : List) =>
+      content(out) == content(in1) ++ Set(v)
+  }
+}
diff --git a/testcases/synthesis/current/List/Split.scala b/testcases/synthesis/current/List/Split.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f37e68264a8b5c4030fa283abc630f22ef98cd6e
--- /dev/null
+++ b/testcases/synthesis/current/List/Split.scala
@@ -0,0 +1,37 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Complete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  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 : BigInt) : BigInt = {
+    if(i < 0) -i else i
+  } ensuring(_ >= 0)
+
+  def split(list : List) : (List,List) = {
+    choose { (res : (List,List)) => splitSpec(list, res) }
+  }
+
+}
diff --git a/testcases/synthesis/current/List/Union.scala b/testcases/synthesis/current/List/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d6a5fa579f5745f00e469f19ee853da15d4fece7
--- /dev/null
+++ b/testcases/synthesis/current/List/Union.scala
@@ -0,0 +1,37 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object Union {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List) : BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1)+ size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    case Cons(i, t) => Set(i) ++ content(t)
+  }
+
+  def insert(in1: List, v: BigInt): List = {
+    Cons(v, in1)
+  } 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/current/Parentheses/Par.scala b/testcases/synthesis/current/Parentheses/Par.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b91213086be4792e9535efb450bca636ca907485
--- /dev/null
+++ b/testcases/synthesis/current/Parentheses/Par.scala
@@ -0,0 +1,54 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.collection._
+
+
+object MatchPar {
+  abstract class AbsChar
+  case object OP extends AbsChar
+  case object CP extends AbsChar
+  case object NA extends AbsChar
+
+  def matchPar(l: List[AbsChar]): BigInt = {
+
+    ???[BigInt]
+    /*
+    l match {
+      case Nil() => 0
+      case Cons(h, t) =>
+        val rec = matchPar(t)
+        h match {
+          case OP => 1 + rec
+          case CP => if (rec <= 0) {
+            -1
+          } else {
+            rec - 1
+          }
+          case NA => rec
+        }
+    }*/
+  } ensuring { res =>
+    ((count(OP, l) != count(CP, l)) ==> (res != 0)) &&
+    ((l, res) passes {
+      case Nil() => 0
+      case Cons(OP, Cons(CP, Nil())) => 0
+      case Cons(CP, Cons(OP, _))     => -1
+      case Cons(OP, Cons(OP, Nil())) => 2
+      case Cons(OP, Cons(OP, Cons(CP, Cons(CP, Cons(OP, Cons(CP, Nil())))))) => 0
+    })
+  }
+
+  def count[T](a: T, l: List[T]): BigInt = {
+    l match {
+      case Cons(h, t) =>
+        if (h == a) {
+          1 + count(a, t)
+        } else {
+          count(a, t)
+        }
+      case Nil() => BigInt(0)
+    }
+  } ensuring { (res: BigInt) =>
+    res >= 0
+  }
+}
diff --git a/testcases/synthesis/current/SortedList/Delete.scala b/testcases/synthesis/current/SortedList/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..788f232d35449cff75ac27442ce7e9cb50f42391
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/Delete.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListDelete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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 delete(in: List, v: BigInt) = {
+    require(isSorted(in))
+
+    choose( (res : List) =>
+        (content(res) == content(in) -- Set(v)) && isSorted(res)
+    )
+  }
+}
diff --git a/testcases/synthesis/current/SortedList/Diff.scala b/testcases/synthesis/current/SortedList/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d391b85ba60e2b405530ddb45b40d94071263725
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/Diff.scala
@@ -0,0 +1,53 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListDiff {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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 delete(in1: List, v: BigInt): 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 diff(in1: List, in2: List) = {
+    require(isSorted(in1) && isSorted(in2))
+
+    choose {
+      (out : List) =>
+        (content(out) == content(in1) -- content(in2)) && isSorted(out)
+    }
+  }
+
+}
diff --git a/testcases/synthesis/current/SortedList/Insert.scala b/testcases/synthesis/current/SortedList/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0bf80d1e99cef290e602b0da905d6966713c77b7
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/Insert.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsert {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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: BigInt): List = {
+    require(isSorted(in1))
+
+    choose { (out : List) =>
+      (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+    }
+  }
+}
diff --git a/testcases/synthesis/current/SortedList/InsertAlways.scala b/testcases/synthesis/current/SortedList/InsertAlways.scala
new file mode 100644
index 0000000000000000000000000000000000000000..73e0b240d776780fab6ac8091a8f0c925c56e695
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/InsertAlways.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsertAlways {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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 insertAlways(in1: List, v: BigInt) = {
+    require(isSorted(in1))
+
+    choose{ (out : List) =>
+      (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+    }
+  }
+}
diff --git a/testcases/synthesis/current/SortedList/InsertionSort.scala b/testcases/synthesis/current/SortedList/InsertionSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0752ad33fe2249de829d7180e6facaab8fb6e160
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/InsertionSort.scala
@@ -0,0 +1,49 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListInsertionSort {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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: BigInt): 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 insertionSort(in1: List): List = {
+    choose { (out: List) =>
+      content(out) == content(in1) && isSorted(out)
+    }
+  }
+}
diff --git a/testcases/synthesis/current/SortedList/MergeSort.scala b/testcases/synthesis/current/SortedList/MergeSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7a285c146ff249a020b6c6611fe55bf3625ecf80
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/MergeSort.scala
@@ -0,0 +1,62 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListUnion {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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 split(in: List): (List, List) = {
+    in match {
+      case Cons(h1, Cons(h2, t)) =>
+        val r = split(t)
+        (Cons(h1, r._1), Cons(h2, r._2))
+      case Cons(h1, Nil) =>
+        (in, Nil)
+      case Nil =>
+        (Nil, Nil)
+    }
+  }
+
+  def merge(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    (in1, in2) match {
+      case (Cons(h1, t1), Cons(h2, t2)) =>
+        if (h1 < h2) {
+          Cons(h1, merge(t1, in2))
+        } else {
+          Cons(h2, merge(in1, t2))
+        }
+      case (l, Nil) => l
+      case (Nil, l) => l
+    }
+  } ensuring {
+    (out : List) =>
+     (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+  }
+
+  def sort(in: List): List = {
+    ???[List]
+  } ensuring {
+    (out : List) =>
+     content(out) == content(in) && isSorted(out)
+  }
+}
diff --git a/testcases/synthesis/current/SortedList/MergeSortGuided.scala b/testcases/synthesis/current/SortedList/MergeSortGuided.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0035eceeadbeea82295a56d06b7ff092e7df3f35
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/MergeSortGuided.scala
@@ -0,0 +1,68 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListUnion {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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 split(in: List): (List, List) = {
+    in match {
+      case Cons(h1, Cons(h2, t)) =>
+        val r = split(t)
+        (Cons(h1, r._1), Cons(h2, r._2))
+      case Cons(h1, Nil) =>
+        (in, Nil)
+      case Nil =>
+        (Nil, Nil)
+    }
+  }
+
+  def merge(in1: List, in2: List): List = {
+    require(isSorted(in1) && isSorted(in2))
+    (in1, in2) match {
+      case (Cons(h1, t1), Cons(h2, t2)) =>
+        if (h1 < h2) {
+          Cons(h1, merge(t1, in2))
+        } else {
+          Cons(h2, merge(in1, t2))
+        }
+      case (l, Nil) => l
+      case (Nil, l) => l
+    }
+  } ensuring {
+    (out : List) =>
+     (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+  }
+
+  def sort(in: List): List = {
+    in match {
+      case Cons(h1, Cons(h2, t)) =>
+        val s = split(in)
+        merge(sort(s._1), sort(s._2))
+      case _ =>
+        ???[List]
+    }
+  } ensuring {
+    (out : List) =>
+     content(out) == content(in) && isSorted(out)
+  }
+}
diff --git a/testcases/synthesis/current/SortedList/Union.scala b/testcases/synthesis/current/SortedList/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d3f11adcccc07e44d1b82c1c6aed7144cb30523c
--- /dev/null
+++ b/testcases/synthesis/current/SortedList/Union.scala
@@ -0,0 +1,51 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object SortedListUnion {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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: BigInt): 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 union(in1: List, in2: List) = {
+    require(isSorted(in1) && isSorted(in2))
+    choose {
+      (out : List) =>
+       (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+    }
+  }
+}
diff --git a/testcases/synthesis/current/StrictSortedList/Delete.scala b/testcases/synthesis/current/StrictSortedList/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..23999d96c3577b80b00b252e0c07509f4b4b2176
--- /dev/null
+++ b/testcases/synthesis/current/StrictSortedList/Delete.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListDelete {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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 delete(in: List, v: BigInt) = {
+    require(isSorted(in))
+
+    choose( (res : List) =>
+        (content(res) == content(in) -- Set(v)) && isSorted(res)
+    )
+  }
+}
diff --git a/testcases/synthesis/current/StrictSortedList/Insert.scala b/testcases/synthesis/current/StrictSortedList/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..65f3c01f9d7b7d8d45136196a6289088df46fa22
--- /dev/null
+++ b/testcases/synthesis/current/StrictSortedList/Insert.scala
@@ -0,0 +1,34 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListInsert {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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: BigInt): List = {
+    require(isSorted(in1))
+
+    choose { (out : List) =>
+      (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+    }
+  }
+}
diff --git a/testcases/synthesis/current/StrictSortedList/Union.scala b/testcases/synthesis/current/StrictSortedList/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c10ed419d3c2cc4fefc9690efb37bc723799ef1c
--- /dev/null
+++ b/testcases/synthesis/current/StrictSortedList/Union.scala
@@ -0,0 +1,51 @@
+import leon.annotation._
+import leon.lang._
+import leon.lang.synthesis._
+
+object StrictSortedListUnion {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case object Nil extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil => BigInt(0)
+    case Cons(_, t) => BigInt(1) + size(t)
+  }) ensuring(res => res >= 0)
+
+  def content(l: List): Set[BigInt] = l match {
+    case Nil => Set.empty[BigInt]
+    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: BigInt): 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 union(in1: List, in2: List) = {
+    require(isSorted(in1) && isSorted(in2))
+    choose {
+      (out : List) =>
+       (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+    }
+  }
+}
diff --git a/testcases/synthesis/current/UnaryNumerals/Add.scala b/testcases/synthesis/current/UnaryNumerals/Add.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a34d1834fbb5cc2418ca830c5576e64d74169b4f
--- /dev/null
+++ b/testcases/synthesis/current/UnaryNumerals/Add.scala
@@ -0,0 +1,21 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsAdd {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n: Num): BigInt = {
+    n match {
+      case Z => BigInt(0)
+      case S(p) => BigInt(1) + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x: Num, y: Num): Num = {
+    choose { (r : Num) =>
+      value(r) == value(x) + value(y)
+    }
+  }
+}
diff --git a/testcases/synthesis/current/UnaryNumerals/Distinct.scala b/testcases/synthesis/current/UnaryNumerals/Distinct.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4287378d1f95225e4ff1ffae57b2d0579d72c3a5
--- /dev/null
+++ b/testcases/synthesis/current/UnaryNumerals/Distinct.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsDistinct {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n: Num): BigInt = {
+    n match {
+      case Z => BigInt(0)
+      case S(p) => BigInt(1) + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x: Num, y: Num): Num = {
+    x match {
+      case S(p) => S(add(p, y))
+      case Z => y
+    }
+  } ensuring { (r : Num) =>
+    value(r) == value(x) + value(y)
+  }
+
+  def distinct(x: Num, y: Num): Num = {
+    choose { (r : Num) =>
+      r != x && r != y
+    }
+  }
+}
diff --git a/testcases/synthesis/current/UnaryNumerals/Mult.scala b/testcases/synthesis/current/UnaryNumerals/Mult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bfa39365e8a8b35555ddc2265f40c775251b8d17
--- /dev/null
+++ b/testcases/synthesis/current/UnaryNumerals/Mult.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+object UnaryNumeralsMult {
+  sealed abstract class Num
+  case object Z extends Num
+  case class  S(pred: Num) extends Num
+
+  def value(n: Num): BigInt = {
+    n match {
+      case Z => BigInt(0)
+      case S(p) => BigInt(1) + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def add(x: Num, y: Num): Num = {
+    x match {
+      case S(p) => S(add(p, y))
+      case Z => y
+    }
+  } ensuring { (r : Num) =>
+    value(r) == value(x) + value(y)
+  }
+
+  def mult(x: Num, y: Num): Num = {
+    choose { (r : Num) =>
+      value(r) == value(x) * value(y)
+    }
+  }
+}
diff --git a/testcases/synthesis/current/run.sh b/testcases/synthesis/current/run.sh
new file mode 100755
index 0000000000000000000000000000000000000000..522e432df0c4244634b71e0358d822eb693de2e2
--- /dev/null
+++ b/testcases/synthesis/current/run.sh
@@ -0,0 +1,43 @@
+#!/bin/bash
+
+function run {
+    cmd="./leon --debug=report --timeout=30 --synthesis --cegis:maxsize=7 $1"
+    echo "Running " $cmd
+    echo "------------------------------------------------------------------------------------------------------------------"
+    $cmd;
+}
+
+echo "==================================================================================================================" >> synthesis-report.txt
+# These are all the benchmarks included in my thesis
+# List
+run testcases/synthesis/current/List/Insert.scala
+run testcases/synthesis/current/List/Delete.scala
+run testcases/synthesis/current/List/Union.scala
+run testcases/synthesis/current/List/Diff.scala
+run testcases/synthesis/current/List/Split.scala
+
+# SortedList
+run testcases/synthesis/current/SortedList/Insert.scala
+run testcases/synthesis/current/SortedList/InsertAlways.scala
+run testcases/synthesis/current/SortedList/Delete.scala
+run testcases/synthesis/current/SortedList/Union.scala
+run testcases/synthesis/current/SortedList/Diff.scala
+run testcases/synthesis/current/SortedList/InsertionSort.scala
+
+# StrictSortedList
+run testcases/synthesis/current/StrictSortedList/Insert.scala
+run testcases/synthesis/current/StrictSortedList/Delete.scala
+run testcases/synthesis/current/StrictSortedList/Union.scala
+
+# UnaryNumerals
+run testcases/synthesis/current/UnaryNumerals/Add.scala
+run testcases/synthesis/current/UnaryNumerals/Distinct.scala
+run testcases/synthesis/current/UnaryNumerals/Mult.scala
+
+# BatchedQueue
+run testcases/synthesis/current/BatchedQueue/Enqueue.scala
+run testcases/synthesis/current/BatchedQueue/Dequeue.scala
+
+# AddressBook
+run testcases/synthesis/current/AddressBook/Make.scala
+run testcases/synthesis/current/AddressBook/Merge.scala