diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation7.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..53d67729fd57723d1693c564e99cd3d66ee095ef
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation7.scala
@@ -0,0 +1,29 @@
+import leon.lang._
+
+object ArrayParamMutation7 {
+
+  def f(i: BigInt)(implicit world: Array[BigInt]): BigInt = {
+    require(world.length == 3)
+
+    world(1) += 1 //global counter of f
+
+    val res = i*i
+    world(0) = res
+    res
+  }
+
+  def mainProgram(): Unit = {
+
+    implicit val world: Array[BigInt] = Array(0,0,0)
+
+    f(1)
+    assert(world(0) == 1)
+    f(2)
+    assert(world(0) == 4)
+    f(4)
+    assert(world(0) == 16)
+
+    assert(world(1) == 3)
+  }
+
+}