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/test2 | |
| 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/test2')
| -rw-r--r-- | Test/test2/strings-no-where.bpl | 2 | ||||
| -rw-r--r-- | Test/test2/strings-where.bpl | 2 |
2 files changed, 2 insertions, 2 deletions
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;
|