diff --git a/src/test/resources/regression/verification/xlang/invalid/Array4.scala b/src/test/resources/regression/verification/purescala/invalid/Array5.scala
similarity index 87%
rename from src/test/resources/regression/verification/xlang/invalid/Array4.scala
rename to src/test/resources/regression/verification/purescala/invalid/Array5.scala
index 111d4e3a49489d45f20f09682ebd8118ffd0e86e..2adb7e5c5e218505f9a391a28739f38abd621e5b 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array4.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array5.scala
@@ -2,7 +2,7 @@
 
 import leon.lang._
 
-object Array4 {
+object Array5 {
 
   def foo(a: Array[Int]): Int = {
     a(2)
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array5.scala b/src/test/resources/regression/verification/purescala/invalid/Array6.scala
similarity index 90%
rename from src/test/resources/regression/verification/xlang/invalid/Array5.scala
rename to src/test/resources/regression/verification/purescala/invalid/Array6.scala
index 32a12648f584e15bf037394bd72a29d23f8cd1a1..18a1e7ab0015edb8aeb4221ccbe7e558520bde85 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array5.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array6.scala
@@ -2,7 +2,7 @@
 
 import leon.lang._
 
-object Array5 {
+object Array6 {
 
   def foo(a: Array[Int]): Int = {
     require(a.length > 2)
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array6.scala b/src/test/resources/regression/verification/purescala/invalid/Array7.scala
similarity index 91%
rename from src/test/resources/regression/verification/xlang/invalid/Array6.scala
rename to src/test/resources/regression/verification/purescala/invalid/Array7.scala
index 5e0aded3317087239fe0726e3ece5fa2f8fafc6d..dcf7059f82c714e941bf757a997405b1e868239c 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array6.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array7.scala
@@ -2,7 +2,7 @@
 
 import leon.lang._
 
-object Array6 {
+object Array7 {
 
   def foo(a: Array[Int]): Int = {
     require(a.length > 0)
diff --git a/src/test/resources/regression/verification/xlang/invalid/Mean.scala b/src/test/resources/regression/verification/purescala/invalid/Mean.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/invalid/Mean.scala
rename to src/test/resources/regression/verification/purescala/invalid/Mean.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested15.scala b/src/test/resources/regression/verification/purescala/invalid/Nested15.scala
similarity index 82%
rename from src/test/resources/regression/verification/xlang/valid/Nested15.scala
rename to src/test/resources/regression/verification/purescala/invalid/Nested15.scala
index 490404f860473b796658c3540fa401aa0a30f157..228afa9fa6a217258aacbb2604817808f2b43abc 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested15.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Nested15.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2015 EPFL, Lausanne */
 import leon.collection._
-object Nested1 {
+object Nested15 {
 
   def foo[A](i: List[A]): BigInt = {
     val n = i
@@ -11,8 +11,7 @@ object Nested1 {
       rec3(l.head).size + j + n.size + i.size
     }
     rec2(List(true, true, false), 2)
-  } ensuring(i.size + 7 == _)
+  } ensuring(_ == i.size + 9) // Should be 2* size
 
 }
 
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/xlang/valid/Array6.scala b/src/test/resources/regression/verification/purescala/valid/Array1.scala
similarity index 93%
rename from src/test/resources/regression/verification/xlang/valid/Array6.scala
rename to src/test/resources/regression/verification/purescala/valid/Array1.scala
index ec477eb30918e469ebc566f2d9aff527fe79056e..4dbec292cbd7d332745c69dee5a6bf54ce782369 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array6.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Array1.scala
@@ -2,7 +2,7 @@
 
 import leon.lang._
 
-object Array6 {
+object Array1 {
 
   def foo(a: Array[Int]): Int = {
     require(a.length > 2 && a(2) == 5)
diff --git a/src/test/resources/regression/verification/xlang/valid/Array8.scala b/src/test/resources/regression/verification/purescala/valid/Array2.scala
similarity index 92%
rename from src/test/resources/regression/verification/xlang/valid/Array8.scala
rename to src/test/resources/regression/verification/purescala/valid/Array2.scala
index 29c1b686c38919014dded81b3ca2610b60aaa23f..53d30e9af2d51257cb3a5ac16487ae15d08a8aac 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array8.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Array2.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2015 EPFL, Lausanne */
 
-object Array8 {
+object Array2 {
 
   def foo(a: Array[Int]): Array[Int] = {
     require(a.length >= 2)
diff --git a/src/test/resources/regression/verification/xlang/valid/Array9.scala b/src/test/resources/regression/verification/purescala/valid/Array3.scala
similarity index 93%
rename from src/test/resources/regression/verification/xlang/valid/Array9.scala
rename to src/test/resources/regression/verification/purescala/valid/Array3.scala
index 10140b9c112d1bc85fab636df0efcdcd5827ee92..b7ea754b4de89d701112d7ab234d0bfa55d90ad5 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array9.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Array3.scala
@@ -1,6 +1,6 @@
 /* Copyright 2009-2015 EPFL, Lausanne */
 
-object Array9 {
+object Array3 {
 
   def foo(i: Int): Array[Int] = {
     require(i > 0)
diff --git a/src/test/resources/regression/verification/xlang/valid/Choose1.scala b/src/test/resources/regression/verification/purescala/valid/Choose2.scala
similarity index 92%
rename from src/test/resources/regression/verification/xlang/valid/Choose1.scala
rename to src/test/resources/regression/verification/purescala/valid/Choose2.scala
index 380be2148ea64fc0ad2ae56040e7bcdcf1b3aabd..ad05bda101385ae70c32663e7d5451e09560a978 100644
--- a/src/test/resources/regression/verification/xlang/valid/Choose1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Choose2.scala
@@ -3,7 +3,7 @@
 import leon.lang._
 import leon.lang.synthesis._
 
-object Choose1 {
+object Choose2 {
 
   def test(x: Int): Int = {
 
diff --git a/src/test/resources/regression/verification/xlang/valid/Mean.scala b/src/test/resources/regression/verification/purescala/valid/Mean.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Mean.scala
rename to src/test/resources/regression/verification/purescala/valid/Mean.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested1.scala b/src/test/resources/regression/verification/purescala/valid/Nested1.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested1.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested1.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested10.scala b/src/test/resources/regression/verification/purescala/valid/Nested10.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested10.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested10.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested11.scala b/src/test/resources/regression/verification/purescala/valid/Nested11.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested11.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested11.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested12.scala b/src/test/resources/regression/verification/purescala/valid/Nested12.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested12.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested12.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested13.scala b/src/test/resources/regression/verification/purescala/valid/Nested13.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested13.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested13.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested14.scala b/src/test/resources/regression/verification/purescala/valid/Nested14.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested14.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested14.scala
diff --git a/src/test/resources/regression/verification/purescala/valid/Nested15.scala b/src/test/resources/regression/verification/purescala/valid/Nested15.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a81c77e67042ac24586fdbe2a45818dcad49ea23
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Nested15.scala
@@ -0,0 +1,17 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.collection._
+object Nested15 {
+
+  def foo[A](i: List[A]): BigInt = {
+    val n = i
+    def rec1[B](j: List[B]) = j ++ j
+    def rec2[C](l: List[C], j: BigInt) = {
+      require(l.nonEmpty)
+      def rec3(k: C) = k :: rec1[C](l)
+      rec3(l.head).size + j + n.size + i.size
+    }
+    rec2(List(true, true, false), 2)
+  } ensuring(_ == 2 * i.size + 9)
+
+}
+
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested2.scala b/src/test/resources/regression/verification/purescala/valid/Nested2.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested2.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested2.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested3.scala b/src/test/resources/regression/verification/purescala/valid/Nested3.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested3.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested3.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested4.scala b/src/test/resources/regression/verification/purescala/valid/Nested4.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested4.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested4.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested5.scala b/src/test/resources/regression/verification/purescala/valid/Nested5.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested5.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested5.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested6.scala b/src/test/resources/regression/verification/purescala/valid/Nested6.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested6.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested6.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested7.scala b/src/test/resources/regression/verification/purescala/valid/Nested7.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested7.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested7.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested8.scala b/src/test/resources/regression/verification/purescala/valid/Nested8.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested8.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested8.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested9.scala b/src/test/resources/regression/verification/purescala/valid/Nested9.scala
similarity index 100%
rename from src/test/resources/regression/verification/xlang/valid/Nested9.scala
rename to src/test/resources/regression/verification/purescala/valid/Nested9.scala
diff --git a/src/test/resources/regression/verification/xlang/invalid/Asserts.scala b/src/test/resources/regression/verification/xlang/invalid/Asserts2.scala
similarity index 93%
rename from src/test/resources/regression/verification/xlang/invalid/Asserts.scala
rename to src/test/resources/regression/verification/xlang/invalid/Asserts2.scala
index 3540c98ddf25ee54132bf523a1d59774c085b100..bfda82471559f5ce6c631cf6fd2ca97cf2bbed06 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Asserts.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Asserts2.scala
@@ -4,7 +4,7 @@ import leon.annotation._
 import leon.lang._
 import leon.lang._
 
-object Asserts {
+object Asserts2 {
 
   def assert1(i: BigInt): BigInt = { // we might define assert like so
     require(i >= 0)