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, 6 insertions, 0 deletions

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index f8b8b82b..9a7fec0c 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -486,6 +486,12 @@ namespace Microsoft.Boogie {
                 case Microsoft.Boogie.BinaryOperator.Opcode.Or:

                   op = " || ";

                   break;

+                case Microsoft.Boogie.BinaryOperator.Opcode.Pow:

+                  op = " ** ";

+                  break;

+                case Microsoft.Boogie.BinaryOperator.Opcode.RealDiv:

+                  op = " / ";

+                  break;

                 case Microsoft.Boogie.BinaryOperator.Opcode.Sub:

                   op = " - ";

                   break;