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)

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index dd5bcff2..bfe185e7 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -268,7 +268,7 @@ implementation p()
 

   A:

     assume {:inferred} true;

-    assume 0 - 1 <= x;

+    assume -1 <= x;

     assume {:inferred} -1 <= x;

     goto B, E;