From 550caf7bc7e6427f26bfb3d24f224e12c6c1c318 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Wed, 1 Jul 2015 13:29:11 -0700
Subject: Fixed bug in BplImp! Improvements in encoding of reads of function
 values.

---
 Binaries/DafnyPrelude.bpl | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'Binaries')

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