diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 610ceb3d672fc4741fe841b1dbe9b61f4b98b0c2..0f512690d094b2a9bdbc3c8ca98e1cc10091fbac 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -280,4 +280,80 @@ object SortedList {
         ))
       ))
   }
+
+  synthesize("Church")("""
+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)
+    }
+  }
+}
+    """) {
+    case "add" =>
+      Apply("ADT Induction on 'y'", List(
+        Apply("CEGIS"),
+        Apply("CEGIS")
+      ))
+  }
+
+  synthesize("Church")("""
+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
+    }
+  }
+}
+    """) {
+    case "distinct" =>
+      Apply("CEGIS")
+  }
 }