diff options
| author |  Rustan Leino <unknown> | 2014-02-23 22:06:56 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-23 22:06:56 -0800 |
| commit | e2f9a3153a2e80c055f9a6d1a2abf8ba9c787009 (patch) | |
| tree | 4f9b4d34c0714bc6a3ab8ff2892f2e6b4acf93a9 /Test/dafny0/Answer | |
| parent | 297f9d4f1b409b2204b536f8393db3f6ccec18e2 (diff) | |
Added another colemma-calls-function-recursively test
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 78d6c126..7b546c36 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1404,7 +1404,8 @@ CoResolution.dfy(132,17): Error: a recursive call from a copredicate can go only CoResolution.dfy(138,17): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(146,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(148,4): Error: a recursive call from a copredicate can go only to other copredicates
-20 resolution/type errors detected in CoResolution.dfy
+CoResolution.dfy(164,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+21 resolution/type errors detected in CoResolution.dfy
-------------------- CoPrefix.dfy --------------------
CoPrefix.dfy(161,3): Error BP5003: A postcondition might not hold on this return path.
|