diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b2.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index 457bc894..7d964061 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -17,7 +17,7 @@ class Benchmark2 { var high := a.Length();
while (low < high)
- invariant 0 <= low && high <= a.Length();
+ invariant 0 <= low && low <= high && high <= a.Length();
invariant (forall i :: 0 <= i && i < low ==> a.Get(i) < key);
invariant (forall i :: high <= i && i < a.Length() ==> key < a.Get(i));
decreases high - low;
|