2 files changed, 7 insertions, 4 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 7a972f22..a6f1e9b7 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -487,20 +487,20 @@ Execution trace:
 Array.dfy(95,18): Error: assertion violation
 Execution trace:
     (0,0): anon0
-Array.dfy(107,6): Error: insufficient reads clause to read array element
+Array.dfy(110,6): Error: insufficient reads clause to read array element
 Execution trace:
     (0,0): anon7_Else
     (0,0): anon8_Then
     (0,0): anon9_Then
-Array.dfy(115,6): Error: insufficient reads clause to read array element
+Array.dfy(118,6): Error: insufficient reads clause to read array element
 Execution trace:
     (0,0): anon7_Else
     (0,0): anon8_Then
     (0,0): anon9_Then
-Array.dfy(131,6): Error: assignment may update an array element not in the enclosing context's modifies clause
+Array.dfy(134,6): Error: assignment may update an array element not in the enclosing context's modifies clause
 Execution trace:
     (0,0): anon0
-Array.dfy(138,6): Error: assignment may update an array element not in the enclosing context's modifies clause
+Array.dfy(141,6): Error: assignment may update an array element not in the enclosing context's modifies clause
 Execution trace:
     (0,0): anon0
 
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 60854f63..5f366d10 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -93,6 +93,9 @@ class A {
     assert y[8] == 30;
     assert y[90] + y[91] + y[0] + 20 == y.Length;
     assert y[93] == 24;  // error (it's 25)
+
+    y[..] := 4; // assign to all elements.
+    assert forall i :: 0 <= i < y.Length ==> y[i] == 4;
   }
 }