diff --git a/testcases/synthesis/ChurchNumerals.scala b/testcases/synthesis/ChurchNumerals.scala
index 229d79945c9736772c1b85264b7fb877665478ca..287e4ecefe9ecb24b43e0d5f0a8fded7cdd8e85f 100644
--- a/testcases/synthesis/ChurchNumerals.scala
+++ b/testcases/synthesis/ChurchNumerals.scala
@@ -18,4 +18,9 @@ object ChurchNumerals {
       value(r) == value(x) + value(y)
     }
   }
+
+  def workingAdd(x : Num, y : Num) : Num = (x match {
+    case Zero() => y
+    case Succ(p) => workingAdd(p, Succ(y))
+  }) ensuring (value(_) == value(x) + value(y))
 }