From 43b80b13bd24bb789849aac3385df6ac4a8233be Mon Sep 17 00:00:00 2001
From: boehmes <unknown>
Date: Thu, 27 Sep 2012 17:13:45 +0200
Subject: Boogie: added type 'real' with overloaded arithmetic operations plus
 real division '/' and (uninterpreted) real exponentiation '**', real literals
 and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod'
 are now mapped to corresponding SMT-LIB operations instead of treating them
 uninterpreted; Made unary minus valid Boogie syntax again (the expression '-
 e' used to be rewritten by the parser to '0 - e', now this is done when
 generating VCs); Extended the BigDec class with additional functionality;
 Added test cases for SMT-LIB prover backend (the Z3 API interface has been
 adapted accordingly, but is untested)

---
 Test/test2/strings-no-where.bpl | 2 +-
 Test/test2/strings-where.bpl    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'Test/test2')

diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl
index c8ef88c8..6aee18ea 100644
--- a/Test/test2/strings-no-where.bpl
+++ b/Test/test2/strings-no-where.bpl
@@ -1,4 +1,4 @@
-type real;
+
 
 type elements;
 
diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl
index 05e392cb..f196899f 100644
--- a/Test/test2/strings-where.bpl
+++ b/Test/test2/strings-where.bpl
@@ -1,4 +1,4 @@
-type real;
+
 
 type elements;
 
-- 
cgit v1.2.3