diff options
author | boehmes <unknown> | 2012-09-27 17:13:45 +0200 |
---|---|---|
committer | boehmes <unknown> | 2012-09-27 17:13:45 +0200 |
commit | 43b80b13bd24bb789849aac3385df6ac4a8233be (patch) | |
tree | 499b3dffd74fd84fdf8aedffacbca424d25680b2 /Test/test20 | |
parent | dfb77ee06c82cf8b9c465f3a2acbc5ceb035c6e5 (diff) |
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)
Diffstat (limited to 'Test/test20')
-rw-r--r-- | Test/test20/Answer | 8 | ||||
-rw-r--r-- | Test/test20/Prog0.bpl | 2 | ||||
-rw-r--r-- | Test/test20/Prog1.bpl | 2 |
3 files changed, 6 insertions, 6 deletions
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;
|