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.)

1 files changed, 4 insertions, 0 deletions

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)) );