1 files changed, 9 insertions, 10 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 8866491e..bc653bd3 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -808,14 +808,7 @@ Basics.dfy(100,16): Error: assertion violation
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Then
-Basics.dfy(113,12): Error: left-hand sides 0 and 1 may refer to the same location
-Execution trace:
-    (0,0): anon0
-    (0,0): anon3
-    (0,0): anon11_Else
-    (0,0): anon6
-    (0,0): anon12_Then
-Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(119,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Then
@@ -824,7 +817,7 @@ Execution trace:
     (0,0): anon6
     (0,0): anon12_Then
     (0,0): anon9
-Basics.dfy(133,10): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(133,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value
 Execution trace:
     (0,0): anon0
 Basics.dfy(145,19): Error: assertion violation
@@ -855,8 +848,14 @@ Execution trace:
     (0,0): anon13_Then
     (0,0): anon8
     (0,0): anon14_Then
+Basics.dfy(226,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value
+Execution trace:
+    (0,0): anon0
+Basics.dfy(251,6): Error: left-hand sides 0 and 1 refer to the same location
+Execution trace:
+    (0,0): anon0
 
-Dafny program verifier finished with 19 verified, 11 errors
+Dafny program verifier finished with 35 verified, 12 errors
 
 -------------------- ControlStructures.dfy --------------------
 ControlStructures.dfy(5,3): Error: missing case in case statement: Blue