1 files changed, 19 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index d9d3a572..289a597d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -402,11 +402,25 @@ Execution trace:
 Dafny program verifier finished with 3 verified, 3 errors
 
 -------------------- ResolutionErrors.dfy --------------------
+ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'class' context
 ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
 ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
 ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
 ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)
-4 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(45,14): Error: a field must be selected via an object, not just a class name
+ResolutionErrors.dfy(46,7): Error: unresolved identifier: F
+ResolutionErrors.dfy(47,14): Error: an instance function must be selected via an object, not just a class name
+ResolutionErrors.dfy(48,7): Error: unresolved identifier: G
+ResolutionErrors.dfy(50,2): Error: member M does not exist in class _default
+ResolutionErrors.dfy(52,2): Error: member N does not exist in class _default
+ResolutionErrors.dfy(55,8): Error: non-function expression is called with parameters
+ResolutionErrors.dfy(56,14): Error: member z does not exist in class Global
+ResolutionErrors.dfy(75,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
+ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
+ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
+18 resolution/type errors detected in ResolutionErrors.dfy
 
 -------------------- Array.dfy --------------------
 Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
@@ -540,6 +554,10 @@ Execution trace:
 
 Dafny program verifier finished with 6 verified, 1 error
 
+-------------------- Basics.dfy --------------------
+
+Dafny program verifier finished with 5 verified, 0 errors
+
 -------------------- ControlStructures.dfy --------------------
 ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
 Execution trace: