1 files changed, 34 insertions, 5 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 3198df33..15cec24f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -484,7 +484,8 @@ ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called w
 ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)
 ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)
 ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)
-44 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts
+45 resolution/type errors detected in ResolutionErrors.dfy
 
 -------------------- ParseErrors.dfy --------------------
 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -1154,8 +1155,15 @@ Execution trace:
     (0,0): anon0
     (0,0): anon4_Else
     (0,0): anon5_Then
+Datatypes.dfy(198,13): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
+Execution trace:
+    (0,0): anon0
+Datatypes.dfy(201,17): Error: destructor 'Car' can only be applied to datatype values constructed by 'XCons'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon6_Then
 
-Dafny program verifier finished with 29 verified, 3 errors
+Dafny program verifier finished with 29 verified, 5 errors
 
 -------------------- TypeAntecedents.dfy --------------------
 TypeAntecedents.dfy(32,13): Error: assertion violation
@@ -1313,12 +1321,33 @@ CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost
 Dafny program verifier finished with 22 verified, 0 errors
 
 -------------------- PredExpr.dfy --------------------
-PredExpr.dfy(23,15): Error: value assigned to a nat must be non-negative
+PredExpr.dfy(4,12): Error: condition in assert expression might not hold
+Execution trace:
+    (0,0): anon3_Else
+PredExpr.dfy(36,15): Error: value assigned to a nat must be non-negative
 Execution trace:
     (0,0): anon6_Else
     (0,0): anon7_Else
-PredExpr.dfy(36,17): Error: condition in assert expression might not hold
+PredExpr.dfy(49,17): Error: condition in assert expression might not hold
 Execution trace:
     (0,0): anon0
+PredExpr.dfy(74,14): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon8_Else
+    (0,0): anon3
+    PredExpr.dfy(73,20): anon10_Else
+    (0,0): anon6
+
+Dafny program verifier finished with 11 verified, 4 errors
+
+-------------------- LetExpr.dfy --------------------
+LetExpr.dfy(5,12): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+LetExpr.dfy(104,21): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon11_Then
 
-Dafny program verifier finished with 9 verified, 2 errors
+Dafny program verifier finished with 13 verified, 2 errors