From 91fa6b7d576a111f39cde20de5d8e612b4d712b5 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Thu, 25 Jun 2015 18:12:53 -0700
Subject: Tried to reduce frame-axiom instantiations by saying the earlier heap
 must be a "heap anchor". Currently, a heap is an anchor if it produced by a
 havoc (but not a direct update).

---
 Test/VSI-Benchmarks/b3.dfy | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'Test/VSI-Benchmarks/b3.dfy')

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index f59b0c3e..d47c4d4d 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -96,7 +96,7 @@ class Benchmark3 {
       if x < m { k := j; m := x; }
       j := j+1;
     }
-    
+
     j := 0;
     while j < k
       invariant j <= k;
@@ -108,10 +108,16 @@ class Benchmark3 {
       RotationLemma(old(q.contents), j, qc0, q.contents);
       j := j+1;
     }
-  
+
     assert j == k;  
     assert q.contents == old(q.contents)[k..] + old(q.contents)[..k];
+    ghost var qq := q.contents;
     m := q.Dequeue();
+    assert q.contents == qq[1..] && m == qq[0];
+    assert [m] + q.contents == qq;
+    assert |old(q.contents)| == |q.contents| + 1;
+
+    assert q.contents == old(q.contents)[k+1..] + old(q.contents)[..k];  
   }
 
   lemma RotationLemma(O: seq, j: nat, A: seq, C: seq)
-- 
cgit v1.2.3