1 files changed, 85 insertions, 0 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 2abd64b2..da82fd59 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1000,3 +1000,88 @@ RefinementErrors.dfy(42,9): Error: Refined class has a member with the same name
 RefinementErrors.dfy(12,10): Error: Refinement methods can only be declared in refinement classes: M
 RefinementErrors.dfy(34,10): Error: Different number of output variables
 6 resolution/type errors detected in RefinementErrors.dfy
+
+-------------------- LoopModifies.dfy --------------------
+LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+    (0,0): anon0
+LoopModifies.dfy(17,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+    (0,0): anon0
+    LoopModifies.dfy(14,4): anon9_LoopHead
+    (0,0): anon9_LoopBody
+    LoopModifies.dfy(14,4): anon10_Else
+    (0,0): anon5
+    LoopModifies.dfy(14,4): anon12_Else
+    (0,0): anon7
+LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+    (0,0): anon0
+    LoopModifies.dfy(42,4): anon9_LoopHead
+    (0,0): anon9_LoopBody
+    LoopModifies.dfy(42,4): anon10_Else
+    (0,0): anon5
+    LoopModifies.dfy(42,4): anon12_Else
+    (0,0): anon7
+LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+    (0,0): anon0
+    LoopModifies.dfy(57,4): anon9_LoopHead
+    (0,0): anon9_LoopBody
+    LoopModifies.dfy(57,4): anon10_Else
+    (0,0): anon5
+    LoopModifies.dfy(57,4): anon12_Else
+    (0,0): anon7
+LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause
+Execution trace:
+    (0,0): anon0
+LoopModifies.dfy(98,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+    (0,0): anon0
+    LoopModifies.dfy(90,4): anon9_LoopHead
+    (0,0): anon9_LoopBody
+    LoopModifies.dfy(90,4): anon10_Else
+    (0,0): anon5
+    LoopModifies.dfy(90,4): anon12_Else
+    (0,0): anon7
+LoopModifies.dfy(146,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+    (0,0): anon0
+    LoopModifies.dfy(134,4): anon17_LoopHead
+    (0,0): anon17_LoopBody
+    LoopModifies.dfy(134,4): anon18_Else
+    (0,0): anon5
+    LoopModifies.dfy(134,4): anon20_Else
+    (0,0): anon7
+    LoopModifies.dfy(139,7): anon21_LoopHead
+    (0,0): anon21_LoopBody
+    LoopModifies.dfy(139,7): anon22_Else
+    (0,0): anon12
+    LoopModifies.dfy(139,7): anon24_Else
+    (0,0): anon14
+LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+    (0,0): anon0
+    LoopModifies.dfy(193,4): anon9_LoopHead
+    (0,0): anon9_LoopBody
+    LoopModifies.dfy(193,4): anon10_Else
+    (0,0): anon5
+    LoopModifies.dfy(193,4): anon12_Else
+    (0,0): anon7
+LoopModifies.dfy(260,10): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+    (0,0): anon0
+    LoopModifies.dfy(248,4): anon17_LoopHead
+    (0,0): anon17_LoopBody
+    LoopModifies.dfy(248,4): anon18_Else
+    (0,0): anon5
+    LoopModifies.dfy(248,4): anon20_Else
+    (0,0): anon7
+    LoopModifies.dfy(256,7): anon21_LoopHead
+    (0,0): anon21_LoopBody
+    LoopModifies.dfy(256,7): anon22_Else
+    (0,0): anon12
+    LoopModifies.dfy(256,7): anon24_Else
+    (0,0): anon14
+
+Dafny program verifier finished with 21 verified, 9 errors