Dafny: Added two additional heuristics for guessing missing loop decreases clauses (for loop guard A!=B and for loop guards with multiple conjuncts)

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];