diff --git a/testcases/synthesis/ChurchNumerals.scala b/testcases/synthesis/ChurchNumerals.scala
new file mode 100644
index 0000000000000000000000000000000000000000..229d79945c9736772c1b85264b7fb877665478ca
--- /dev/null
+++ b/testcases/synthesis/ChurchNumerals.scala
@@ -0,0 +1,21 @@
+import leon.Utils._
+object ChurchNumerals {
+  sealed abstract class Num
+  case class Zero() extends Num
+  case class Succ(pred:Num) extends Num
+
+  def value(n:Num) : Int = {
+    n match {
+      case Zero() => 0
+      case Succ(p) => 1 + value(p)
+    }
+  } ensuring (_ >= 0)
+
+  def succ(n:Num) : Num = Succ(n) ensuring(value(_) == value(n) + 1)
+
+  def add(x:Num, y:Num):Num = {
+    choose { (r : Num) => 
+      value(r) == value(x) + value(y)
+    }
+  }
+}