diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b2.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b2.dfy | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy index fd20a72b..1021ee85 100644 --- a/Test/VSI-Benchmarks/b2.dfy +++ b/Test/VSI-Benchmarks/b2.dfy @@ -14,7 +14,6 @@ class Benchmark2 { invariant 0 <= low && low <= high && high <= |a|;
invariant (forall i :: 0 <= i && i < low ==> a[i] < key);
invariant (forall i :: high <= i && i < |a| ==> key < a[i]);
- decreases high - low;
{
var mid := low + (high - low) / 2;
var midVal := a[mid];
|