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)

---
 Source/VCExpr/BigLiteralAbstracter.cs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Source/VCExpr/BigLiteralAbstracter.cs')

diff --git a/Source/VCExpr/BigLiteralAbstracter.cs b/Source/VCExpr/BigLiteralAbstracter.cs
index 7eb93541..879ab6d6 100644
--- a/Source/VCExpr/BigLiteralAbstracter.cs
+++ b/Source/VCExpr/BigLiteralAbstracter.cs
@@ -120,7 +120,7 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Ensures(Contract.Result<VCExpr>() != null);
 
       if (lit.IsNegative)
-        return Gen.Function(VCExpressionGenerator.SubOp,
+        return Gen.Function(VCExpressionGenerator.SubIOp,
                             Gen.Integer(BigNum.ZERO), RepresentPos(lit.Neg));
       else
         return RepresentPos(lit);
@@ -145,7 +145,7 @@ namespace Microsoft.Boogie.VCExprAST {
         BigNum dist = lit - Literals[index - 1].Key;
         if (dist < resDistance) {
           resDistance = dist;
-          res = Gen.Function(VCExpressionGenerator.AddOp,
+          res = Gen.Function(VCExpressionGenerator.AddIOp,
                              Literals[index - 1].Value, Gen.Integer(dist));
         }
       }
@@ -154,7 +154,7 @@ namespace Microsoft.Boogie.VCExprAST {
         BigNum dist = Literals[index].Key - lit;
         if (dist < resDistance) {
           resDistance = dist;
-          res = Gen.Function(VCExpressionGenerator.SubOp,
+          res = Gen.Function(VCExpressionGenerator.SubIOp,
                              Literals[index].Value, Gen.Integer(dist));
         }
       }
@@ -198,7 +198,7 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Requires(bExpr != null);
 
       BigNum dist = bValue - aValue;
-      VCExpr distExpr = Gen.Function(VCExpressionGenerator.SubOp, bExpr, aExpr);
+      VCExpr distExpr = Gen.Function(VCExpressionGenerator.SubIOp, bExpr, aExpr);
       if (dist <= ConstantDistanceTPO)
         // constants that are sufficiently close to each other are put
         // into a precise relationship
-- 
cgit v1.2.3