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, 2 deletions

diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy
index da1f63bb..0e6aff05 100644
--- a/Test/vacid0/SparseArray.dfy
+++ b/Test/vacid0/SparseArray.dfy
@@ -55,7 +55,6 @@ class SparseArray<T> {
       // TODO: why doesn't this work instead of the next line?  invariant (forall x :: x in s ==> x == zero);

       invariant (forall i :: 0 <= i && i < |s| ==> s[i] == zero);

       invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);

-      decreases N - k;

     {

       s := s + [zero];

       id := id + [k];

@@ -110,7 +109,6 @@ class SparseArray<T> {
     var i := 0;

     while (i < n)

       invariant i <= n && |arr| == i;

-      decreases n - i;

     {

       var g: G;

       arr := arr + [g];