diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b7.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b7.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy index 13a8ccd2..95267823 100644 --- a/Test/VSI-Benchmarks/b7.dfy +++ b/Test/VSI-Benchmarks/b7.dfy @@ -36,7 +36,7 @@ class Stream { function Valid():bool
reads this, footprint;
{
- !(null in footprint) && this in footprint && isOpen
+ null !in footprint && this in footprint && isOpen
}
method GetCount() returns (c:int)
@@ -152,7 +152,7 @@ class Client { var wr:= new Stream;
call wr.Create();
while (0<|q.contents|)
- invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && !(q in wr.footprint);
+ invariant wr.Valid() && fresh(wr.footprint) && fresh(q) && q !in wr.footprint;
decreases |q.contents|;
{
call ch:= q.Dequeue();
|