diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation9.scala b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f5046b6cf3b40382ccc5d989d81d73bc577da9f7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayParamMutation9.scala
@@ -0,0 +1,22 @@
+import leon.lang._
+
+object ArrayParamMutation9 {
+  def abs(a: Array[Int]) {
+    require(a.length > 0)
+    var i = 0;
+    (while (i < a.length) {
+      a(i) = if (a(i) < 0) -a(i) else a(i)  // <-- this makes Leon crash
+      i = i + 1
+    }) invariant(i >= 0)
+  }
+
+
+  def main = {
+    val a = Array(0, -1, 2, -3)
+
+    abs(a)
+
+    a(0) + a(1) - 1 + a(2) - 2 + a(3) - 3 // == 0
+  }
+
+}