Fixed bug in BplImp!

Improvements in encoding of reads of function values.

1 files changed, 8 insertions, 0 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index dbf9b76c..2ca10f73 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -273,6 +273,8 @@ const unique class._System.set: ClassName;
 const unique class._System.seq: ClassName;

 const unique class._System.multiset: ClassName;

 

+function Tclass._System.object(): Ty;

+

 function /*{:never_pattern true}*/ dtype(ref): Ty; // changed from ClassName to Ty

 

 function TypeTuple(a: ClassName, b: ClassName): ClassName;

@@ -287,6 +289,12 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }
 

 type HandleType;

 

+function SetRef_to_SetBox(s: [ref]bool): Set Box;

+axiom (forall s: [ref]bool, bx: Box :: { SetRef_to_SetBox(s)[bx] }

+  SetRef_to_SetBox(s)[bx] == s[$Unbox(bx): ref]);

+axiom (forall s: [ref]bool :: { SetRef_to_SetBox(s) }

+  $Is(SetRef_to_SetBox(s), TSet(Tclass._System.object())));

+

 // ---------------------------------------------------------------

 // -- Datatypes --------------------------------------------------

 // ---------------------------------------------------------------