diff --git a/build.sbt b/build.sbt
index 0e3e147a10e395fb58a0ebb3f981b9919deb56b9..4ecb2f93a06874f11e1b9bdd69d8b82530f65ce8 100644
--- a/build.sbt
+++ b/build.sbt
@@ -109,8 +109,8 @@ Keys.fork in run := true
 
 lazy val testSettings = Seq(
     //Keys.fork := true,
-    logBuffered := true,
-    parallelExecution := true
+    logBuffered := false,
+    parallelExecution := false
     //testForkedParallel := true,
     //javaOptions ++= Seq("-Xss64M", "-Xmx4G")
 )
diff --git a/src/main/scala/leon/xlang/AntiAliasingPhase.scala b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
index a7adbfbaad618f79e930e9302fa8733515b198fb..f9610904ce4d8af594cec320532f435d4d6fdadc 100644
--- a/src/main/scala/leon/xlang/AntiAliasingPhase.scala
+++ b/src/main/scala/leon/xlang/AntiAliasingPhase.scala
@@ -262,7 +262,6 @@ object AntiAliasingPhase extends TransformationPhase {
       }
     }
 
-
     def invocEffects(fi: FunctionInvocation): Set[Identifier] = {
       if(!effects.isDefinedAt(fi.tfd.fd)) {
         println("fi not defined: " + fi)
@@ -276,7 +275,6 @@ object AntiAliasingPhase extends TransformationPhase {
       }.toSet
     }
 
-
     rec()
     effects
   }
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation1.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f0e622c66c31e4fe01ff8be5c1b08e17d4d330eb
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation1.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object ArrayParamMutation1 {
+
+  def update(a: Array[BigInt]): Unit = {
+    require(a.length > 0)
+    a(0) = 10
+  }
+
+  def f(): BigInt = {
+    val a = Array.fill(10)(BigInt(0))
+    update(a)
+    a(0)
+  } ensuring(res => res == 10)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation2.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..801b35e0cc545f160fc8061e34fd0ee06b7c3f73
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation2.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object ArrayParamMutation2 {
+
+  def rec(a: Array[BigInt]): BigInt = {
+    require(a.length > 1 && a(0) >= 0)
+    if(a(0) == 0) 
+      a(1)
+    else {
+      a(0) = a(0) - 1
+      a(1) = a(1) + a(0)
+      rec(a)
+    }
+  } ensuring(res => a(0) == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation3.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f575167444f839c0ee900a35de5e4e822624dc21
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation3.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object ArrayParamMutation3 {
+
+  def odd(a: Array[BigInt]): Boolean = {
+    require(a.length > 0 && a(0) >= 0)
+    if(a(0) == 0) false
+    else {
+      a(0) = a(0) - 1
+      even(a)
+    }
+  } ensuring(res => a(0) == 0)
+
+  def even(a: Array[BigInt]): Boolean = {
+    require(a.length > 0 && a(0) >= 0)
+    if(a(0) == 0) true
+    else {
+      a(0) = a(0) - 1
+      odd(a)
+    }
+  } ensuring(res => a(0) == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation4.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..31af4cd5885ea66a2d11e9387ba7e306423ec4d7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation4.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object ArrayParamMutation4 {
+
+  def multipleArgs(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+    require(a1.length > 0 && a2.length > 0)
+    if(a1(0) == 10)
+      a2(0) = 13
+    else
+      a2(0) = a1(0) + 1
+  }
+
+  def transitiveEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+    require(a1.length > 0 && a2.length > 0)
+    multipleArgs(a1, a2)
+  } ensuring(_ => a2(0) >= a1(0))
+
+  def transitiveReverseEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+    require(a1.length > 0 && a2.length > 0)
+    multipleArgs(a2, a1)
+  } ensuring(_ => a1(0) >= a2(0))
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation5.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..249a79d1f3b7d8df8c941ab3121c4eafed149e03
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation5.scala
@@ -0,0 +1,21 @@
+
+import leon.lang._
+
+object ArrayParamMutation5 {
+
+  def mutuallyRec1(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+    require(a1.length > 0 && a1(0) > 0 && a2.length > 0)
+    if(a1(0) == 10) {
+      ()
+    } else {
+      mutuallyRec2(a1, a2)
+    }
+  } ensuring(res => a1(0) == 10)
+
+  def mutuallyRec2(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+    require(a1.length > 0 && a2.length > 0 && a1(0) > 0)
+    a1(0) = 10
+    mutuallyRec1(a1, a2)
+  }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation6.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..29ded427fa6546a103d8da6f98cefc1415f389a6
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation6.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object ArrayParamMutation6 {
+
+  def multipleEffects(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+    require(a1.length > 0 && a2.length > 0)
+    a1(0) = 11
+    a2(0) = 12
+  } ensuring(_ => a1(0) != a2(0))
+
+  def f(a1: Array[BigInt], a2: Array[BigInt]): Unit = {
+    require(a1.length > 0 && a2.length > 0)
+    multipleEffects(a1, a2)
+  } ensuring(_ => a1(0) == 11 && a2(0) == 12)
+
+}