diff --git a/mytest/Capture.scala b/mytest/Capture.scala
deleted file mode 100644
index c1c4c7e1ef466b27f8232afbb67d22e98fb48077..0000000000000000000000000000000000000000
--- a/mytest/Capture.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-object Capture {
-
-  def foo(i: Int): Int = {
-    val a = 3
-    def rec(j: Int): Int = if(j == a) 0 else 1
-    rec(3)
-  }
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/mytest/Match.scala b/mytest/Match.scala
deleted file mode 100644
index 5376cc61d1df009da2c8ba09ea2c57c3bf248cd7..0000000000000000000000000000000000000000
--- a/mytest/Match.scala
+++ /dev/null
@@ -1,18 +0,0 @@
-object Match {
-
-  sealed abstract class A
-  case class B(b: Int) extends A
-  case class C(c: Int) extends A
-
-  def foo(a: A): Int = ({
-
-    var i = 0
-    var j = 0
-
-    {i = i + 1; a} match {
-      case B(b) => {i = i + 1; b}
-      case C(c) => {j = j + 1; i = i + 1; c}
-    }
-    i
-  }) ensuring(_ == 2)
-}
diff --git a/mytest/NAryOp.scala b/mytest/NAryOp.scala
deleted file mode 100644
index adf6c84bfff520ebe720011612b52ec66d9c12dc..0000000000000000000000000000000000000000
--- a/mytest/NAryOp.scala
+++ /dev/null
@@ -1,12 +0,0 @@
-object NAryOp {
-
-  def foo(): Int = ({
-
-    var a = 2
-    bar({a = a + 1; a}, {a = 5 - a; a}, {a = a + 2; a})
-  }) ensuring(_ == 9)
-
-
-  def bar(i1: Int, i2: Int, i3: Int): Int = i1 + i2 + i3
-
-}
diff --git a/mytest/ValSideEffect.scala b/mytest/ValSideEffect.scala
deleted file mode 100644
index 5beefdaffa48d1cdff604c70dcfba5e2fa481db5..0000000000000000000000000000000000000000
--- a/mytest/ValSideEffect.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-object ValSideEffect {
-
-  def foo(): Int = ({
-
-    var a = 2
-    var a2 = 1
-
-    val b = {a = a + 1; a2 = a2 + 1; a} + {a = 5 - a; a}
-    a = a + 1
-    a2 = a2 + 3
-    a + a2 + b
-  }) ensuring(_ == 13)
-
-
-}
-
-// vim: set ts=4 sw=4 et:
diff --git a/mytest/WhileTest.scala b/mytest/WhileTest.scala
deleted file mode 100644
index c080552e54f5861c1ad368ce4c132e957e9e8554..0000000000000000000000000000000000000000
--- a/mytest/WhileTest.scala
+++ /dev/null
@@ -1,20 +0,0 @@
-import leon.Utils._
-
-object WhileTest {
-//  object InvariantFunction {
-//    def invariant(x: Boolean): Unit = ()
-//  }
-//  implicit def while2Invariant(u: Unit) = InvariantFunction
-  def foo(x : Int) : Int = {
-    require(x >= 0)
-
-    var y : Int = x
-
-    (while (y >= 0) {
-      y = y - 1
-      // assert(y >= -1)
-    }) invariant(y >= -1)
-
-    y + 1
-  } ensuring(_ == 0)
-}
diff --git a/mytest/Abs.scala b/testcases/Abs.scala
similarity index 100%
rename from mytest/Abs.scala
rename to testcases/Abs.scala
diff --git a/mytest/BubbleFun.scala b/testcases/BubbleFun.scala
similarity index 100%
rename from mytest/BubbleFun.scala
rename to testcases/BubbleFun.scala
diff --git a/mytest/BubbleWeakInvariant.scala b/testcases/BubbleWeakInvariant.scala
similarity index 100%
rename from mytest/BubbleWeakInvariant.scala
rename to testcases/BubbleWeakInvariant.scala
diff --git a/mytest/MaxSum.scala b/testcases/MaxSum.scala
similarity index 100%
rename from mytest/MaxSum.scala
rename to testcases/MaxSum.scala
diff --git a/mytest/Assign1.scala b/testcases/regression/Assign1.scala
similarity index 100%
rename from mytest/Assign1.scala
rename to testcases/regression/Assign1.scala
diff --git a/mytest/IfExpr1.scala b/testcases/regression/IfExpr1.scala
similarity index 100%
rename from mytest/IfExpr1.scala
rename to testcases/regression/IfExpr1.scala
diff --git a/testcases/regression/Nested2.scala b/testcases/regression/Nested2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..30830df0b22bd2d51892e8e4103c71003844ad63
--- /dev/null
+++ b/testcases/regression/Nested2.scala
@@ -0,0 +1,15 @@
+object Nested2 {
+
+  def foo(i: Int): Int = {
+    val n = 2
+    def rec1(j: Int) = i + j + n
+    def rec2(j: Int) = {
+      def rec3(k: Int) = k + j + i
+      rec3(5)
+    }
+    rec2(2)
+  } ensuring(i + 7 == _)
+
+}
+
+// vim: set ts=4 sw=4 et: