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/test20/Answer    | 8 ++++----
 Test/test20/Prog0.bpl | 2 +-
 Test/test20/Prog1.bpl | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'Test/test20')

diff --git a/Test/test20/Answer b/Test/test20/Answer
index efa5bced..fa33507e 100644
--- a/Test/test20/Answer
+++ b/Test/test20/Answer
@@ -118,7 +118,7 @@ axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3));
 
 const intSet1: Set int;
 
-axiom (forall x: int :: intSet1[x] == (x == 0 - 5 || x == 3));
+axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3));
 
 procedure P();
 
@@ -126,7 +126,7 @@ procedure P();
 
 implementation P()
 {
-    assert (forall x: int :: union(intSet0, intSet1)[x] == (x == 0 - 5 || x == 0 || x == 2 || x == 3));
+    assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3));
 }
 
 
@@ -143,7 +143,7 @@ axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3);
 
 const intSet1: Set int;
 
-axiom (forall x: int :: intSet1[x] <==> x == 0 - 5 || x == 3);
+axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3);
 
 procedure P();
 
@@ -151,7 +151,7 @@ procedure P();
 
 implementation P()
 {
-    assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == 0 - 5 || x == 0 || x == 2 || x == 3);
+    assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3);
 }
 
 
diff --git a/Test/test20/Prog0.bpl b/Test/test20/Prog0.bpl
index ea71b8a8..8fc7b7c7 100644
--- a/Test/test20/Prog0.bpl
+++ b/Test/test20/Prog0.bpl
@@ -1,5 +1,5 @@
 // Let's test some Boogie 2 features ...
-type real;
+
 type elements;
 
 type Field a;
diff --git a/Test/test20/Prog1.bpl b/Test/test20/Prog1.bpl
index 1d75805c..0e9413c1 100644
--- a/Test/test20/Prog1.bpl
+++ b/Test/test20/Prog1.bpl
@@ -1,5 +1,5 @@
 // Let's test some Boogie 2 features ...
-type real;
+
 type elements;
 
 type Field a;
-- 
cgit v1.2.3