diff --git a/testcases/xplusone.scala b/testcases/xplusone.scala
new file mode 100644
index 0000000000000000000000000000000000000000..94e9dfcc855a6878b21bebf9c8241243c4b2d871
--- /dev/null
+++ b/testcases/xplusone.scala
@@ -0,0 +1,21 @@
+import leon.Utils._
+
+object xplusone {
+
+  def f(n : Int) : Int = {
+    if (n > 0) {
+      f(n-1) + 1
+    } else 1
+  } ensuring (rec => rec == n + 1)
+
+  def Sf(n : Int, rec : Int) : Boolean = {
+    if (n > 0) {
+      val res = epsilon((x:Int) => true)
+      Sf(n - 1, res)
+      (rec == res + 1)
+    } else {
+      rec == 1
+    }
+  } ensuring (_ == (rec == n + 1))
+
+}