Merge

1 files changed, 7 insertions, 1 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index fdfdf823..1eb22708 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -645,6 +645,12 @@ Dafny program verifier finished with 7 verified, 1 error
 -------------------- Modules0.dfy --------------------

 Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

 Modules0.dfy(13,7): Error: module T named among imports does not exist

+Modules0.dfy(196,8): Error: Duplicate name of top-level declaration: WazzupA

+Modules0.dfy(197,11): Error: Duplicate name of top-level declaration: WazzupA

+Modules0.dfy(198,7): Error: Duplicate name of top-level declaration: WazzupA

+Modules0.dfy(201,7): Error: Duplicate name of top-level declaration: WazzupB

+Modules0.dfy(202,8): Error: Duplicate name of top-level declaration: WazzupB

+Modules0.dfy(203,11): Error: Duplicate name of top-level declaration: WazzupB

 Modules0.dfy(24,7): Error: import graph contains a cycle: H -> I -> J -> G

 Modules0.dfy(51,8): Error: inter-module calls must follow the module import relation (so module X2 must transitively import YY)

 Modules0.dfy(62,9): Error: inter-module calls must follow the module import relation (so module X1 must transitively import X2)

@@ -656,7 +662,7 @@ Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification
 Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts

 Modules0.dfy(148,10): Error: match source expression 'tree' has already been used as a match source expression in this context

 Modules0.dfy(187,12): Error: match source expression 'l' has already been used as a match source expression in this context

-13 resolution/type errors detected in Modules0.dfy

+19 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

 Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0