Merge branch 'master' of laragit.epfl.ch:projects/leon-2.0

PERMISSIONS

@@ -12,5 +12,5 @@ tail -2 "$0" | ssh git@laragit.epfl.ch setperms ${thisrepo}
 exit $_
 
 # **Do not** add new lines after the following two!
-WRITERS kuncak psuter rblanc edarulov hojjat
+WRITERS kuncak psuter rblanc edarulov hojjat ekneuss kandhada
 READERS @lara mazimmer hardy amin

testcases/xplusone.scala

+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))
+
+}