diff --git a/src/test/resources/regression/verification/xlang/valid/Nested15.scala b/src/test/resources/regression/verification/xlang/valid/Nested15.scala
new file mode 100644
index 0000000000000000000000000000000000000000..490404f860473b796658c3540fa401aa0a30f157
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested15.scala
@@ -0,0 +1,18 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.collection._
+object Nested1 {
+
+  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(i.size + 7 == _)
+
+}
+
+// vim: set ts=4 sw=4 et: