From d2d39ff37467249c3dcb7b9318b71955d62330bf Mon Sep 17 00:00:00 2001
From: Unknown <namin@idea>
Date: Thu, 4 Jul 2013 00:54:04 -0700
Subject: Computations!

Generates 'computing' axioms for both all formals and just decreasing formals.
Supported are literal datatypes, booleans and numbers.
The axioms are given a weight of 10, which seems enough for Z3 to give up when
it is sane to do so.
---
 Binaries/DafnyPrelude.bpl | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'Binaries/DafnyPrelude.bpl')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 5d0b647f..349da0fd 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -7,6 +7,12 @@
 const $$Language$Dafny: bool;  // To be recognizable to the ModelViewer as
 axiom $$Language$Dafny;        // coming from a Dafny program.
 
+// ---------------------------------------------------------------
+// -- Literals ---------------------------------------------------
+// ---------------------------------------------------------------
+function {:identity} Lit<T>(x: T): T { x }
+axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
+
 // ---------------------------------------------------------------
 // -- References -------------------------------------------------
 // ---------------------------------------------------------------
-- 
cgit v1.2.3