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).

---
 Binaries/DafnyPrelude.bpl | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'Binaries/DafnyPrelude.bpl')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index ef6106e0..dbf9b76c 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -398,7 +398,8 @@ function {:inline true} read<alpha>(H:Heap, r:ref, f:Field alpha): alpha { H[r,
 function {:inline true} update<alpha>(H:Heap, r:ref, f:Field alpha, v:alpha): Heap { H[r,f := v] }
 
 function $IsGoodHeap(Heap): bool;
-var $Heap: Heap where $IsGoodHeap($Heap);
+function $IsHeapAnchor(Heap): bool;
+var $Heap: Heap where $IsGoodHeap($Heap) && $IsHeapAnchor($Heap);
 
 function $HeapSucc(Heap, Heap): bool;
 axiom (forall<alpha> h: Heap, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) }
-- 
cgit v1.2.3