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

1 files changed, 2 insertions, 1 deletions

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