diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-27 13:30:28 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-27 13:30:28 -0700 |
| commit | a8bdd2aa3fcbff708b233ee321b13a17f232ce19 (patch) | |
| tree | e58e60ba287a06120df947269220a122455e6402 /Test/dafny0/Answer | |
| parent | e065edad49e5690522fa83a65c88b52cad0a3970 (diff) | |
Dafny: added resolution tests cases for inductive datatypes
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index ed69d5db..762bdea8 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1266,8 +1266,9 @@ Dafny program verifier finished with 32 verified, 6 errors -------------------- Coinductive.dfy --------------------
Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
-Coinductive.dfy(51,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
-3 resolution/type errors detected in Coinductive.dfy
+Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
+Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
+4 resolution/type errors detected in Coinductive.dfy
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
|