From 736969063f99babb854a2ac7c2c2b0d11a8fc253 Mon Sep 17 00:00:00 2001 From: leino Date: Sat, 24 Oct 2015 17:43:46 -0700 Subject: In method and iterator specifications, inline top-level predicates (except protected predicated in cross-module calls) like in other places. --- Test/dafny2/SnapshotableTrees.dfy.expect | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'Test/dafny2') diff --git a/Test/dafny2/SnapshotableTrees.dfy.expect b/Test/dafny2/SnapshotableTrees.dfy.expect index 808fe0f9..68b4ff73 100644 --- a/Test/dafny2/SnapshotableTrees.dfy.expect +++ b/Test/dafny2/SnapshotableTrees.dfy.expect @@ -1,8 +1,15 @@ SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold. SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold. +SnapshotableTrees.dfy(545,15): Related location +Execution trace: + (0,0): anon0 + (0,0): anon3_Then +SnapshotableTrees.dfy(68,23): Error BP5002: A precondition for this call might not hold. +SnapshotableTrees.dfy(648,15): Related location: This is the precondition that might not hold. +SnapshotableTrees.dfy(548,18): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -Dafny program verifier finished with 65 verified, 1 error +Dafny program verifier finished with 65 verified, 2 errors Compiled assembly into SnapshotableTrees.exe -- cgit v1.2.3