diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-07-10 16:52:09 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-07-10 16:52:09 -0700 |
| commit | 92cced2f7bde488e450fa12f7ef50d98f474ab61 (patch) | |
| tree | d9cc893bc1289d8ad09b21f6a2242d31fa51ef70 /Test/dafny0/OpaqueFunctions.dfy.expect | |
| parent | 129ab22811996b4b46cfbcc6eb3f4b97a95f5416 (diff) | |
Make reveal axioms from opaque functions quantify over layers
Diffstat (limited to 'Test/dafny0/OpaqueFunctions.dfy.expect')
| -rw-r--r-- | Test/dafny0/OpaqueFunctions.dfy.expect | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/Test/dafny0/OpaqueFunctions.dfy.expect b/Test/dafny0/OpaqueFunctions.dfy.expect index 9d4497dc..df076f60 100644 --- a/Test/dafny0/OpaqueFunctions.dfy.expect +++ b/Test/dafny0/OpaqueFunctions.dfy.expect @@ -71,5 +71,17 @@ Execution trace: OpaqueFunctions.dfy(138,12): Error: assertion violation
Execution trace:
(0,0): anon0
+OpaqueFunctions.dfy(202,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+OpaqueFunctions.dfy(218,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+OpaqueFunctions.dfy(170,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+OpaqueFunctions.dfy(185,20): Error: assertion violation
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 45 verified, 19 errors
+Dafny program verifier finished with 59 verified, 23 errors
|