1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny0/Matrix-OOB.dfy b/Test/dafny0/Matrix-OOB.dfy
new file mode 100644
index 00000000..d7aacd79
--- /dev/null
+++ b/Test/dafny0/Matrix-OOB.dfy
@@ -0,0 +1,13 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This is a regression test: OOB errors for matrices used to be reported on the
+// quantifier that introduced the variables that constituted the invalid indices.
+
+// WISH: It would be even better to report the error on the variables inside the
+// array instead of the array itself.
+
+method M(m: array2<int>)
+  requires m != null
+  ensures forall i, j :: m[i, j] == 0
+{ }