diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b3.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index d45db684..37b73cba 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -61,10 +61,10 @@ class Benchmark3 { var n := 0;
while (n < |q.contents|)
- invariant n <=|q.contents| ;
- invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
+ invariant n <= |q.contents|;
invariant n == |p|;
- decreases |q.contents| -n;
+ invariant (forall i: int :: 0 <= i && i < n ==> p[i] == i);
+ decreases |q.contents| - n;
{
p := p + [n];
n := n + 1;
|