From fadc6a922eb99b83b898b55286e48f63ed0df751 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 11 Jun 2010 02:02:36 +0000
Subject: Dafny:  Added two additional heuristics for guessing missing loop
 decreases clauses (for loop guard A!=B and for loop guards with multiple
 conjuncts)

---
 Test/vacid0/SparseArray.dfy | 2 --
 1 file changed, 2 deletions(-)

(limited to 'Test/vacid0')

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];
-- 
cgit v1.2.3