Initial set of files.

1 files changed, 16 insertions, 0 deletions

diff --git a/Test/test0/Arrays1.bpl b/Test/test0/Arrays1.bpl
new file mode 100644
index 00000000..db12ecb3
--- /dev/null
+++ b/Test/test0/Arrays1.bpl
@@ -0,0 +1,16 @@
+var Q: [int,int][int]int;

+

+procedure P()

+{

+  var q: [int]int;

+

+  start:

+    // here's how to do it:

+    q := Q[5,8];

+    q[13] := 21;

+    Q[5,8] := q;

+

+    // not like this:

+    Q[5,8][13] := 21;  // error: the updated array must be an identifier

+    return;

+}