summaryrefslogtreecommitdiff
path: root/Test/dafny2
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/dafny2
parentd5685d5afcd053a0bb2178425e1b1d12cd85eb52 (diff)
Snapshot, to be continued
Diffstat (limited to 'Test/dafny2')
-rw-r--r--Test/dafny2/SnapshotableTrees.dfy.expect2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect
index d84bdc45..849b9e38 100644
--- a/Test/dafny2/SnapshotableTrees.dfy.expect
+++ b/Test/dafny2/SnapshotableTrees.dfy.expect
@@ -1,4 +1,4 @@
-SnapshotableTrees.dfy(68,16): Error BP5002: A precondition for this call might not hold.
+SnapshotableTrees.dfy(68,24): Error BP5002: A precondition for this call might not hold.
SnapshotableTrees.dfy(648,16): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0