diff --git a/testcases/synthesis/sygus/duration.scala b/testcases/synthesis/sygus/duration.scala
new file mode 100644
index 0000000000000000000000000000000000000000..06a9b9cd52c0d6a3e1aa5a9280c74bf37791b707
--- /dev/null
+++ b/testcases/synthesis/sygus/duration.scala
@@ -0,0 +1,65 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Times {
+  case class Hour(v: BigInt) {
+    def isValid = v >= 0// && v < 24
+    def toSeconds = v*3600
+  }
+
+  case class Minute(v: BigInt) {
+    def isValid = v >= 0 && v < 60
+    def toSeconds = v*60
+  }
+
+  case class Second(v: BigInt) {
+    def isValid = v >= 0 && v < 60
+    def toSeconds = v
+  }
+
+  case class Time(h: Hour, m: Minute, s: Second) {
+    def isValid = {
+      h.isValid && m.isValid && s.isValid
+    }
+
+    def toSeconds = h.toSeconds + m.toSeconds + s.toSeconds
+  }
+
+  def incTime(t: Time, k: BigInt) = {
+    choose((tres: Time, seconds: BigInt) => seconds == t.toSeconds && seconds + k == tres.toSeconds && tres.isValid)
+  }
+
+  def incTimeInlined(h: BigInt, m: BigInt, s: BigInt, inc: BigInt) = {
+    require(
+      h >= 0 &&
+      m >= 0 && m < 60 &&
+      s >= 0 && s < 60 &&
+      inc > 0
+    )
+
+    choose { (hres: BigInt, mres: BigInt, sres: BigInt) =>
+      hres >= 0 &&
+      mres >= 0 && mres < 60 &&
+      sres >= 0 && sres < 60 &&
+      ((hres*3600+mres*60+sres) == ((h*3600 + m*60 + s) + inc))
+    }
+  }
+
+  def incTime2(m: BigInt, s: BigInt, inc: BigInt) = {
+    require(
+      m >= 0 &&
+      s >= 0 && s < 60 &&
+      inc > 0
+    )
+
+    ???[(BigInt, BigInt)]
+
+  } ensuring { (res: (BigInt, BigInt)) =>
+    val (mres, sres) = res
+
+    mres >= 0 &&
+    sres >= 0 && sres < 60 &&
+    ((mres*60+sres) == ((m*60 + s) + inc))
+  }
+}
diff --git a/testcases/synthesis/sygus/mirror.scala b/testcases/synthesis/sygus/mirror.scala
new file mode 100644
index 0000000000000000000000000000000000000000..79528809a40cd01ba64e4345f36d2ffecf6b3b1f
--- /dev/null
+++ b/testcases/synthesis/sygus/mirror.scala
@@ -0,0 +1,42 @@
+import leon._
+import leon.lang._
+import leon.collection._
+import leon.lang.synthesis._
+
+object Mirror {
+
+  def inttuple(a: BigInt, b: BigInt): (BigInt, BigInt) = {
+    ???[(BigInt, BigInt)]
+  } ensuring {
+    out => out._1+1 == a && out._2-1 == b
+  }
+
+  def tuple(a: List[BigInt], b: List[BigInt]): (List[BigInt], List[BigInt]) = {
+    ???[(List[BigInt], List[BigInt])]
+  } ensuring {
+    out => out._1 == a && out._2 == b
+  }
+
+  def mirror1(a: List[BigInt], b: List[BigInt]): (List[BigInt], List[BigInt]) = {
+    ???[(List[BigInt], List[BigInt])]
+  } ensuring {
+    out => out._1 == b && out._2 == a
+  }
+
+  def mirror2[T](a: List[T], b: List[T]): (List[T], List[T]) = {
+    ???[(List[T], List[T])]
+  } ensuring {
+    out => out._1 == b && out._2 == a
+  }
+
+  def transfer(a: List[BigInt], b: List[BigInt]): (List[BigInt], List[BigInt]) = {
+    ???[(List[BigInt], List[BigInt])]
+  } ensuring {
+    out =>
+      (a, b) match {
+        case (Cons(ah, at), b) => (out._2.head == (ah + 1)) && (out._2.tail == b)
+        case _ => true
+      }
+  }
+
+}