diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-08-15 11:46:59 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-08-15 11:46:59 -0700 |
| commit | 2ef4d9e637e0633347c4030b50925a92f8c12963 (patch) | |
| tree | 5c4f4e0997ce6b7fcbaa50d7b0dcb3e621011b83 /Test/hofs/ReadsReads.dfy.expect | |
| parent | 9eeeaeb525173d6322f929f630587ebb6ca0b201 (diff) | |
Refactor resolver, and really allow reads to take fields of type A -> set<obj>
twoState and codeContext is moved to a new class ResolveOpts
Diffstat (limited to 'Test/hofs/ReadsReads.dfy.expect')
| -rw-r--r-- | Test/hofs/ReadsReads.dfy.expect | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect index e83e017c..f1da2003 100644 --- a/Test/hofs/ReadsReads.dfy.expect +++ b/Test/hofs/ReadsReads.dfy.expect @@ -36,4 +36,4 @@ Execution trace: ReadsReads.dfy(95,16): anon15_Else
(0,0): anon21_Then
-Dafny program verifier finished with 13 verified, 9 errors
+Dafny program verifier finished with 17 verified, 9 errors
|