diff --git a/PERMISSIONS b/PERMISSIONS
index 20019048dd418bfd5e6eba56ffaa50c6a279e1d3..cfb16377c7bc961ddb3d8d433ab9e746c44b8772 100755
--- a/PERMISSIONS
+++ b/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
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))
+
+}