Fix: multi-dimensional OOB errors were sometimes reported on incorrect locations.

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..2e5c0366
--- /dev/null
+++ b/Test/dafny0/Matrix-OOB.dfy
@@ -0,0 +1,13 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /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

+{ }