From be556deb1f82b9e16b7337422d80a2546559648e Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 13 Feb 2014 15:32:48 -0800
Subject: Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom
 for literals. Added axiom to better handle DtAlloc/GenericAlloc
 correspondence (which improves handling of computations).

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

(limited to 'Binaries/DafnyPrelude.bpl')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 1069f419..d4c97f0f 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -646,6 +646,9 @@ axiom (forall b: BoxType, h: HeapType, t: BoxType ::
 axiom (forall b: BoxType, h: HeapType ::
   { GenericAlloc(b, h), DtAlloc($Unbox(b): DatatypeType, h) }
   GenericAlloc(b, h) <==> DtAlloc($Unbox(b): DatatypeType, h));
+axiom (forall dt: DatatypeType, h: HeapType ::
+  { GenericAlloc($Box(dt), h) }
+  GenericAlloc($Box(dt), h) <==> DtAlloc(dt, h));
 // ==> GenericAlloc
 axiom (forall b: bool, h: HeapType ::
   $IsGoodHeap(h) ==> GenericAlloc($Box(b), h));
-- 
cgit v1.2.3