From 54542194373c8a44263821ed2e4dbf94b82313f4 Mon Sep 17 00:00:00 2001
From: Mario Bucev <mario.bucev@epfl.ch>
Date: Wed, 3 Jan 2024 14:07:44 +0100
Subject: [PATCH] Fix MatchError in EffectsAnalyzer

---
 .../imperative/EffectsAnalyzer.scala          |  2 +-
 .../valid/MutableArrayFieldInTrait.scala      | 35 +++++++++++++++++++
 2 files changed, 36 insertions(+), 1 deletion(-)
 create mode 100644 frontends/benchmarks/imperative/valid/MutableArrayFieldInTrait.scala

diff --git a/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala b/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala
index 2fbdd9d6e..77d5ad5d5 100644
--- a/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala
+++ b/core/src/main/scala/stainless/extraction/imperative/EffectsAnalyzer.scala
@@ -392,7 +392,7 @@ trait EffectsAnalyzer extends oo.CachingPhase {
         case (tt: TupleType, TupleFieldAccessor(idx) +: xs) =>
           0 < idx && idx <= tt.dimension && rec(tt.bases(idx - 1), xs)
 
-        case (ArrayType(base), ArrayAccessor(idx) +: xs) =>
+        case (ArrayType(base), (ArrayAccessor(_) | UnknownArrayAccessor) +: xs) =>
           rec(base, xs)
 
         case (_, Nil) =>
diff --git a/frontends/benchmarks/imperative/valid/MutableArrayFieldInTrait.scala b/frontends/benchmarks/imperative/valid/MutableArrayFieldInTrait.scala
new file mode 100644
index 000000000..81f855d81
--- /dev/null
+++ b/frontends/benchmarks/imperative/valid/MutableArrayFieldInTrait.scala
@@ -0,0 +1,35 @@
+import stainless.annotation._
+import stainless.lang._
+import StaticChecks._
+
+object MutableArrayFieldInTrait {
+  case class Buffer(arr: Array[Byte])
+
+  @mutable
+  trait MyTrait {
+    val buf: Buffer
+
+    final def modify: Unit = {
+      if (buf.arr.length >= 10) buf.arr(0) = 1
+    }
+  }
+  case class MyClass(buf: Buffer) extends MyTrait
+
+  def modify(buf: Buffer, i: Int): Unit = {
+    require(0 <= i && i < buf.arr.length)
+    buf.arr(i) = 42
+  }
+
+  def test(mt: MyTrait, i: Int, j: Int, k: Int): Unit = {
+    require(0 <= i && i < mt.buf.arr.length)
+    require(0 <= j && j < mt.buf.arr.length)
+    require(0 <= k && k < mt.buf.arr.length)
+    require(i != j && j != k && i != k)
+    val oldi = mt.buf.arr(i)
+    modify(mt.buf, j)
+    mt.buf.arr(k) = 24
+    assert(mt.buf.arr(i) == oldi)
+    assert(mt.buf.arr(j) == 42)
+    assert(mt.buf.arr(k) == 24)
+  }
+}
\ No newline at end of file