diff options
author | rustanleino <unknown> | 2010-06-11 02:02:36 +0000 |
---|---|---|
committer | rustanleino <unknown> | 2010-06-11 02:02:36 +0000 |
commit | fadc6a922eb99b83b898b55286e48f63ed0df751 (patch) | |
tree | 8aa3e8fa417e79fdfc96502ddcb5a5fdc13c7927 /Test/VSI-Benchmarks/b2.dfy | |
parent | 9521767199e98aafb780421b859da3fb8773af42 (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];
|