From 316b123de766e9cba492b573be5b11c1ef25927c Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Tue, 31 Jul 2012 17:56:14 +0200
Subject: [PATCH] recursion elim
---
testcases/xplusone.scala | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
create mode 100644 testcases/xplusone.scala
diff --git a/testcases/xplusone.scala b/testcases/xplusone.scala
new file mode 100644
index 000000000..94e9dfcc8
--- /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))
+
+}
--
GitLab