diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b5.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b5.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy index 8026e60f..34ff5f57 100644 --- a/Test/VSI-Benchmarks/b5.dfy +++ b/Test/VSI-Benchmarks/b5.dfy @@ -17,8 +17,8 @@ class Queue<T> { tail.next == null &&
(forall n ::
n in spine ==>
- n != null && n.Valid() &&
- n.footprint <= footprint &&
+ n != null && n.footprint <= footprint && this !in n.footprint &&
+ n.Valid() &&
(n.next == null ==> n == tail)) &&
(forall n ::
n in spine ==>
|