summaryrefslogtreecommitdiff
path: root/Test/dafny0/Answer
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/Answer')
-rw-r--r--Test/dafny0/Answer8
1 files changed, 7 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 15cec24f..9de11371 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -640,6 +640,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)
@@ -651,7 +657,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