more testing

src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation1.scala

+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)
+
+}

src/test/resources/regression/verification/xlang/valid/NestedFunParamsMutation2.scala

+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)
+
+}

src/test/resources/regression/xlang/error/ArrayAliasing10.scala

+/* 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)
+  }
+
+}