3 files changed, 7 insertions, 7 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index ecde4fb1..358a64bf 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1617,15 +1617,13 @@ TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive met
 
 -------------------- IteratorResolution.dfy --------------------
 IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field
-IteratorResolution.dfy(60,11): Error: LHS of assignment does not denote a mutable field
 IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int)
 IteratorResolution.dfy(76,19): Error: RHS (of type bool) not assignable to LHS (of type int)
 IteratorResolution.dfy(79,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called
 IteratorResolution.dfy(83,15): Error: logical negation expects a boolean argument (instead got int)
 IteratorResolution.dfy(17,11): Error: LHS of assignment does not denote a mutable field
-IteratorResolution.dfy(18,11): Error: LHS of assignment does not denote a mutable field
 IteratorResolution.dfy(19,12): Error: LHS of assignment does not denote a mutable field
-9 resolution/type errors detected in IteratorResolution.dfy
+7 resolution/type errors detected in IteratorResolution.dfy
 
 -------------------- Iterators.dfy --------------------
 Iterators.dfy(36,14): Error BP5002: A precondition for this call might not hold.
diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy
index dca4cb93..68fec344 100644
--- a/Test/dafny0/IteratorResolution.dfy
+++ b/Test/dafny0/IteratorResolution.dfy
@@ -15,7 +15,7 @@ module Mx {
   method IteratorUser() {
     var iter := new ExampleIterator.ExampleIterator(15);
     iter.k := 12;  // error: not allowed to assign to iterator's in-parameters
-    iter.x := 12;  // error: not allowed to assign to iterator's yield-parameters
+    iter.x := 12;  // note, not allowed to assign to iterator's yield-parameters (except via 'this')
     iter.xs := [];  // error: not allowed to assign to iterator's yield-history variables
     var j := 0;
     while (j < 100) {
@@ -57,7 +57,7 @@ module Mx {
       requires g0.u;
     {
       g0.t := true;  // error: not allowed to assign to .t
-      g0.u := true;  // error: not allowed to assign to .u
+      g0.u := true;  // note, not allowed to assign to iterator's yield-parameters (except via 'this'), but this is checked by the verifier
       var g1 := new GenericIterator.GenericIterator(20);
       assert g1.u < 200;  // .u is an integer
 
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
index 680c2812..3f06e445 100644
--- a/Test/dafny0/Iterators.dfy
+++ b/Test/dafny0/Iterators.dfy
@@ -91,10 +91,11 @@ method TestIterA()
 iterator IterB(c: Cell)
   requires c != null;
   modifies c;
-  yield ensures c.data == old(c.data);  // error: cannot prove this without a reads clause
+  yield ensures c.data == old(c.data);
   ensures true;
 {
   if (*) { yield; }
+  if (*) { yield; }  // error: cannot prove the yield-ensures clause here (needs a reads clause)
   c.data := *;
 }
 
@@ -117,10 +118,11 @@ iterator IterC(c: Cell)
   requires c != null;
   modifies c;
   reads c;
-  yield ensures c.data == old(c.data);  // error: cannot prove this without a reads clause
+  yield ensures c.data == old(c.data);
   ensures true;
 {
   if (*) { yield; }
+  if (*) { yield; }  // this time, all is fine, because the iterator has an appropriate reads clause
   c.data := *;
 }