summaryrefslogtreecommitdiff
path: root/Test/hofs/Field.dfy.expect
diff options
context:
space:
mode:
authorGravatar leino <unknown>2014-12-02 14:04:53 -0800
committerGravatar leino <unknown>2014-12-02 14:04:53 -0800
commit682a34e72274aff3ef4ebcbe54244d1c2ca0ba2f (patch)
tree448289d84b91a081f7658710f0fcb9cc425805c8 /Test/hofs/Field.dfy.expect
parentd5685d5afcd053a0bb2178425e1b1d12cd85eb52 (diff)
Snapshot, to be continued
Diffstat (limited to 'Test/hofs/Field.dfy.expect')
-rw-r--r--Test/hofs/Field.dfy.expect8
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/hofs/Field.dfy.expect b/Test/hofs/Field.dfy.expect
index 927d8b06..9f6998f5 100644
--- a/Test/hofs/Field.dfy.expect
+++ b/Test/hofs/Field.dfy.expect
@@ -1,14 +1,14 @@
-Field.dfy(12,10): Error: assertion violation
-Execution trace:
- (0,0): anon0
Field.dfy(12,12): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
-Field.dfy(21,10): Error: assertion violation
+Field.dfy(12,15): Error: assertion violation
Execution trace:
(0,0): anon0
Field.dfy(21,12): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
+Field.dfy(21,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
Dafny program verifier finished with 2 verified, 4 errors