diff options
Diffstat (limited to 'Test/dafny1/SchorrWaite-stages.dfy')
| -rw-r--r-- | Test/dafny1/SchorrWaite-stages.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy index 5a4da8ce..094e7be7 100644 --- a/Test/dafny1/SchorrWaite-stages.dfy +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -213,9 +213,9 @@ ghost module M2 refines M1 { // references, we need to make sure we can deal with the proof obligation for the path
// argument. For this reason, we add invariants that say that "path" and the .pathFromRoot
// field of all marked nodes contain values that make sense in the pre-state.
- invariant old(allocated(path)) && old(ReachableVia(root, path, t, S));
+ invariant !fresh(path) && old(ReachableVia(root, path, t, S));
invariant forall n :: n in S && n.marked ==> var pth := n.pathFromRoot;
- old(allocated(pth)) && old(ReachableVia(root, pth, n, S));
+ !fresh(pth) && old(ReachableVia(root, pth, n, S));
invariant forall n :: n in S && n.marked ==> old(Reachable(root, n, S));
decreases *; // keep postponing termination checking
|