From 92991242c8ea361b8da5a83bd19462b216387618 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 10 Jun 2014 18:15:59 -0700
Subject: Specialized Lit function for int and real (leaving all other cases
 polymorphic). This reduces the number of int<->U conversions that Boogie
 adds, which avoids a looping problem in Z3. (Regrettably, the test suite
 seems to have become rather unstable. Sometimes everything verifies and
 sometimes there is some looping forever.)

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

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 3d993797..3f508c81 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -10,6 +10,10 @@ axiom $$Language$Dafny;        // coming from a Dafny program.
 // ---------------------------------------------------------------
 // -- Literals ---------------------------------------------------
 // ---------------------------------------------------------------
+function {:identity} LitInt(x: int): int { x }
+axiom (forall x: int :: { $Box(LitInt(x)) } $Box(LitInt(x)) == Lit($Box(x)) );
+function {:identity} LitReal(x: real): real { x }
+axiom (forall x: real :: { $Box(LitReal(x)) } $Box(LitReal(x)) == Lit($Box(x)) );
 function {:identity} Lit<T>(x: T): T { x }
 axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
 
-- 
cgit v1.2.3