diff options
| author |  Rustan Leino <unknown> | 2013-12-17 13:56:41 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-12-17 13:56:41 -0800 |
| commit | 679af7cd0963341cbb057cf9049c81b515a8fa26 (patch) | |
| tree | fc796b17831d924689c491583c0efd9203edad77 /Test/dafny0/Answer | |
| parent | bbf809e2a1a474e6e79b1c02faa42ec22af8ac8c (diff) | |
Don't inline opaque functions.
Added a verifying example with opaque functions and explicit proofs.
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 676c0313..3b475659 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1785,8 +1785,11 @@ OpaqueFunctions.dfy(119,14): Error: assertion violation Execution trace:
(0,0): anon0
(0,0): anon6_Else
+OpaqueFunctions.dfy(135,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 32 verified, 18 errors
+Dafny program verifier finished with 37 verified, 19 errors
-------------------- Maps.dfy --------------------
Maps.dfy(76,8): Error: element may not be in domain
|