diff options
author | 2010-06-11 02:02:36 +0000 | |
---|---|---|
committer | 2010-06-11 02:02:36 +0000 | |
commit | d0411d08eba6e800509744dbb9e0b4c380964e9b (patch) | |
tree | b67726e5eb114d28fc8af048344f16ed8eed71bd /Test/VSI-Benchmarks/b2.dfy | |
parent | 5dddcccf78dbd7752963c5fe9da288697ccd27eb (diff) |
Dafny: Added two additional heuristics for guessing missing loop decreases clauses (for loop guard A!=B and for loop guards with multiple conjuncts)
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];
|