diff --git a/src/test/resources/regression/xlang/error/NestedFunctionAliasing1.scala b/src/test/resources/regression/xlang/error/NestedFunctionAliasing1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..12feace5413c23e688ac194192482120793b4e24
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/NestedFunctionAliasing1.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object NestedFunctinAliasing1 {
+
+  def f(): Int = {
+    val a = Array(1,2,3,4)
+
+    def g(b: Array[Int]): Unit = {
+      require(b.length > 0 && a.length > 0)
+      b(0) = 10
+      a(0) = 17
+    } ensuring(_ => b(0) == 10)
+
+    g(a)
+    a(0)
+  } ensuring(_ == 10)
+}
diff --git a/src/test/resources/regression/xlang/error/NestedFunctionAliasing2.scala b/src/test/resources/regression/xlang/error/NestedFunctionAliasing2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..81a9b82b39fb47af105ef2e3122fe86a8b10dbb6
--- /dev/null
+++ b/src/test/resources/regression/xlang/error/NestedFunctionAliasing2.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object NestedFunctinAliasing1 {
+
+  def f(a: Array(1,2,3,4)): Int = {
+
+    def g(b: Array[Int]): Unit = {
+      require(b.length > 0 && a.length > 0)
+      b(0) = 10
+      a(0) = 17
+    } ensuring(_ => b(0) == 10)
+
+    g(a)
+    a(0)
+  } ensuring(_ == 10)
+
+}