diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a7250a7bcfd572c49584110d213f9e9991a10c9f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object NestedFunParamsMutation1 {
+
+  def f(): Int = {
+    def g(a: Array[Int]): Unit = {
+      require(a.length > 0)
+      a(0) = 10
+    }
+
+    val a = Array(1,2,3,4)
+    g(a)
+    a(0)
+  } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..799a87c6e9e70bf6ef89bfc1fb7a6e116adb7feb
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala
@@ -0,0 +1,21 @@
+import leon.lang._
+
+object NestedFunParamsMutation2 {
+
+  def f(): Int = {
+    def g(a: Array[Int]): Unit = {
+      require(a.length > 0)
+      a(0) = 10
+    }
+
+    def h(a: Array[Int]): Unit = {
+      require(a.length > 0)
+      g(a)
+    }
+
+    val a = Array(1,2,3,4)
+    h(a)
+    a(0)
+  } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/xlang/error/ArrayAliasing10.scala b/src/test/resources/regression/xlang/error/ArrayAliasing10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..05737b03d9816be72cf52f4913f57a482abf76dd
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/ArrayAliasing10.scala
@@ -0,0 +1,19 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object ArrayAliasing10 {
+
+  def foo(): Int = {
+    val a = Array.fill(5)(0)
+
+    def rec(): Array[Int] = {
+      
+      def nestedRec(): Array[Int] = {
+        a
+      }
+      nestedRec()
+    }
+    val b = rec()
+    b(0)
+  }
+
+}