From 9da78cff0c7f13a8a1615ad63fc927311d63f1ef Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 25 Aug 2014 11:28:53 -0700
Subject: Fixed bugs in previous check-in Made up for inadequacy in reasoning
 machinery (supplying Int(Real(i)) == i axiom)

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

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index bf9ef568..993ada51 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -432,7 +432,11 @@ axiom (forall o: ref :: 0 <= _System.array.Length(o));
 // -- Reals ------------------------------------------------------
 // ---------------------------------------------------------------
 
-function {:inline true} _System.real.Trunc(x: real): int { int(x) }
+function Int(x: real): int { int(x) }
+function Real(x: int): real { real(x) }
+axiom (forall i: int :: { Int(Real(i)) } Int(Real(i)) == i);
+
+function {:inline true} _System.real.Trunc(x: real): int { Int(x) }
 
 // ---------------------------------------------------------------
 // -- The heap ---------------------------------------------------
-- 
cgit v1.2.3