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)

7 files changed, 286 insertions, 39 deletions

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

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 1561aec0..3035c9de 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -328,6 +328,8 @@ namespace Microsoft.Boogie.VCExprAST {
         }

       } else if (node.Val is BigNum) {

         return Gen.Integer(node.asBigNum);

+      } else if (node.Val is BigDec) {

+        return Gen.Real(node.asBigDec);

       } else if (node.Val is BvConst) {

         return Gen.Bitvector((BvConst)node.Val);

       } else {

@@ -961,8 +963,20 @@ namespace Microsoft.Boogie.VCExprAST {
     public VCExpr Visit(UnaryOperator unaryOperator) {

       //Contract.Requires(unaryOperator != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

-      Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Not && this.args.Count == 1);

-      return Gen.Not(this.args);

+      Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Neg || unaryOperator.Op == UnaryOperator.Opcode.Not);

+      Contract.Assert(this.args.Count == 1);

+      if (unaryOperator.Op == UnaryOperator.Opcode.Neg) {

+        VCExpr e = cce.NonNull(this.args[0]);

+        if (cce.NonNull(e.Type).IsInt) {

+          return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);

+        }

+        else {

+          return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);

+        }

+      }

+      else {

+        return Gen.Not(this.args);

+      }

     }

 

     public VCExpr Visit(BinaryOperator binaryOperator) {

@@ -996,6 +1010,21 @@ namespace Microsoft.Boogie.VCExprAST {
       return this.args[0];

     }

 

+    public VCExpr Visit(ArithmeticCoercion arithCoercion) {

+      //Contract.Requires(arithCoercion != null);

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

+      Contract.Assert(this.args.Count == 1);

+      switch (arithCoercion.Coercion) {

+        case ArithmeticCoercion.CoercionType.ToInt:

+          return Gen.Function(VCExpressionGenerator.ToIntOp, this.args);

+        case ArithmeticCoercion.CoercionType.ToReal:

+          return Gen.Function(VCExpressionGenerator.ToRealOp, this.args);

+        default:

+          Contract.Assert(false);

+          return null;

+      }

+    }

+

     public VCExpr Visit(IfThenElse ite) {

       //Contract.Requires(ite != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

@@ -1012,15 +1041,42 @@ namespace Microsoft.Boogie.VCExprAST {
 

       switch (app.Op) {

         case BinaryOperator.Opcode.Add:

-          return Gen.Function(VCExpressionGenerator.AddOp, args);

+          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {

+            return Gen.Function(VCExpressionGenerator.AddIOp, args);

+          }

+          else {

+            return Gen.Function(VCExpressionGenerator.AddROp, args);

+          }

         case BinaryOperator.Opcode.Sub:

-          return Gen.Function(VCExpressionGenerator.SubOp, args);

+          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {

+            return Gen.Function(VCExpressionGenerator.SubIOp, args);

+          }

+          else {

+            return Gen.Function(VCExpressionGenerator.SubROp, args);

+          }

         case BinaryOperator.Opcode.Mul:

-          return Gen.Function(VCExpressionGenerator.MulOp, args);

+          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {

+            return Gen.Function(VCExpressionGenerator.MulIOp, args);

+          }

+          else {

+            return Gen.Function(VCExpressionGenerator.MulROp, args);

+          }

         case BinaryOperator.Opcode.Div:

-          return Gen.Function(VCExpressionGenerator.DivOp, args);

+          return Gen.Function(VCExpressionGenerator.DivIOp, args);

         case BinaryOperator.Opcode.Mod:

           return Gen.Function(VCExpressionGenerator.ModOp, args);

+        case BinaryOperator.Opcode.RealDiv:

+          VCExpr arg0 = cce.NonNull(args[0]);

+          VCExpr arg1 = cce.NonNull(args[1]);

+          if (cce.NonNull(arg0.Type).IsInt) {

+            arg0 = Gen.Function(VCExpressionGenerator.ToRealOp, arg0);

+          }

+          if (cce.NonNull(arg1.Type).IsInt) {

+            arg1 = Gen.Function(VCExpressionGenerator.ToRealOp, arg1);

+          }

+          return Gen.Function(VCExpressionGenerator.DivROp, arg0, arg1);

+        case BinaryOperator.Opcode.Pow:

+          return Gen.Function(VCExpressionGenerator.PowOp, args);

         case BinaryOperator.Opcode.Eq:

         case BinaryOperator.Opcode.Iff:

           // we don't distinguish between equality and equivalence at this point

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index 848fafcb..02e3adda 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -376,6 +376,13 @@ namespace Microsoft.Boogie.VCExprAST {
     internal const string intMulName = "*";

     internal const string intDivName = "/";

     internal const string intModName = "%";

+    internal const string realAddName = "realAdd";

+    internal const string realSubName = "realSub";

+    internal const string realMulName = "realMul";

+    internal const string realDivName = "realDiv";

+    internal const string realPowName = "realPow";

+    internal const string toIntName = "toIntCoercion";

+    internal const string toRealName = "toRealCoercion";

 

     internal void AssertAsTerm(string x, LineariserOptions options) {

       Contract.Requires(options != null);

@@ -928,10 +935,16 @@ namespace Microsoft.Boogie.VCExprAST {
       public bool VisitAddOp(VCExprNAry node, LineariserOptions options) {

         //Contract.Requires(options != null);

         //Contract.Requires(node != null);

-        if (CommandLineOptions.Clo.ReflectAdd) {

-          WriteTermApplication(intAddNameReflect, node, options);

-        } else {

-          WriteTermApplication(intAddName, node, options);

+        if (node.Type.IsInt) {

+          if (CommandLineOptions.Clo.ReflectAdd) {

+            WriteTermApplication(intAddNameReflect, node, options);

+          }

+          else {

+            WriteTermApplication(intAddName, node, options);

+          }

+        }

+        else {

+          WriteTermApplication(realAddName, node, options);

         }

         return true;

       }

@@ -939,14 +952,24 @@ namespace Microsoft.Boogie.VCExprAST {
       public bool VisitSubOp(VCExprNAry node, LineariserOptions options) {

         //Contract.Requires(options != null);

         //Contract.Requires(node != null);

-        WriteTermApplication(intSubName, node, options);

+        if (node.Type.IsInt) {

+          WriteTermApplication(intSubName, node, options);

+        }

+        else {

+          WriteTermApplication(realSubName, node, options);

+        }

         return true;

       }

 

       public bool VisitMulOp(VCExprNAry node, LineariserOptions options) {

         //Contract.Requires(options != null);

         //Contract.Requires(node != null);

-        WriteTermApplication(intMulName, node, options);

+        if (node.Type.IsInt) {

+          WriteTermApplication(intMulName, node, options);

+        }

+        else {

+          WriteTermApplication(realMulName, node, options);

+        }

         return true;

       }

 

@@ -964,6 +987,20 @@ namespace Microsoft.Boogie.VCExprAST {
         return true;

       }

 

+      public bool VisitRealDivOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        WriteTermApplication(realDivName, node, options);

+        return true;

+      }

+

+      public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        WriteTermApplication(realPowName, node, options);

+        return true;

+      }

+

       public bool VisitLtOp(VCExprNAry node, LineariserOptions options) {

         //Contract.Requires(options != null);

         //Contract.Requires(node != null);

@@ -1006,6 +1043,20 @@ namespace Microsoft.Boogie.VCExprAST {
         return true;

       }

 

+      public bool VisitToIntOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        WriteApplication(toIntName, node, options);

+        return true;

+      }

+

+      public bool VisitToRealOp(VCExprNAry node, LineariserOptions options) {

+        //Contract.Requires(options != null);

+        //Contract.Requires(node != null);

+        WriteApplication(toRealName, node, options);

+        return true;

+      }

+

       public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {

         //Contract.Requires(options != null);

         //Contract.Requires(node != null);

diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs
index fb91d326..9d366c9f 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -524,6 +524,7 @@ namespace Microsoft.Boogie.TypeErasure {
 

     public virtual void Setup() {

       GetBasicTypeRepr(Type.Int);

+      GetBasicTypeRepr(Type.Real);

       GetBasicTypeRepr(Type.Bool);

     }

 

@@ -625,6 +626,7 @@ namespace Microsoft.Boogie.TypeErasure {
       base.Setup();

 

       GetTypeCasts(Type.Int);

+      GetTypeCasts(Type.Real);

       GetTypeCasts(Type.Bool);

     }

 

@@ -730,7 +732,7 @@ namespace Microsoft.Boogie.TypeErasure {
     ////////////////////////////////////////////////////////////////////////////

 

     // the only types that we allow in "untyped" expressions are U,

-    // Type.Int, and Type.Bool

+    // Type.Int, Type.Real, and Type.Bool

 

     public override Type TypeAfterErasure(Type type) {

       //Contract.Requires(type != null);

@@ -746,7 +748,7 @@ namespace Microsoft.Boogie.TypeErasure {
     [Pure]

     public override bool UnchangedType(Type type) {

       //Contract.Requires(type != null);

-      return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);

+      return type.IsInt || type.IsReal || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);

     }

 

     public VCExpr Cast(VCExpr expr, Type toType) {

@@ -1143,7 +1145,7 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Requires(bindings != null);

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

-      Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int);

+      Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int || node.Type == Type.Real);

       return node;

     }

 

@@ -1360,7 +1362,7 @@ namespace Microsoft.Boogie.TypeErasure {
     }

 

     // Cast the arguments of the node to their old type if necessary and possible; otherwise use

-    // their new type (int, bool, or U)

+    // their new type (int, real, bool, or U)

     private VCExpr CastArgumentsToOldType(VCExprNAry node, VariableBindings bindings, int newPolarity) {

       Contract.Requires(bindings != null);

       Contract.Requires(node != null);

@@ -1448,19 +1450,19 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Requires((bindings != null));

       Contract.Requires((node != null));

       Contract.Ensures(Contract.Result<VCExpr>() != null);

-      return CastArguments(node, Type.Int, bindings, 0);

+      return CastArguments(node, node.Type, bindings, 0);

     }

     public override VCExpr VisitSubOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

       Contract.Requires((node != null));

       Contract.Ensures(Contract.Result<VCExpr>() != null);

-      return CastArguments(node, Type.Int, bindings, 0);

+      return CastArguments(node, node.Type, bindings, 0);

     }

     public override VCExpr VisitMulOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

       Contract.Requires((node != null));

       Contract.Ensures(Contract.Result<VCExpr>() != null);

-      return CastArguments(node, Type.Int, bindings, 0);

+      return CastArguments(node, node.Type, bindings, 0);

     }

     public override VCExpr VisitDivOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

@@ -1474,29 +1476,41 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Ensures(Contract.Result<VCExpr>() != null);

       return CastArguments(node, Type.Int, bindings, 0);

     }

+    public override VCExpr VisitRealDivOp(VCExprNAry node, VariableBindings bindings) {

+      Contract.Requires((bindings != null));

+      Contract.Requires((node != null));

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

+      return CastArguments(node, Type.Real, bindings, 0);

+    }

+    public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) {

+      Contract.Requires((bindings != null));

+      Contract.Requires((node != null));

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

+      return CastArguments(node, Type.Real, bindings, 0);

+    }

     public override VCExpr VisitLtOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

       Contract.Requires((node != null));

       Contract.Ensures(Contract.Result<VCExpr>() != null);

-      return CastArguments(node, Type.Int, bindings, 0);

+      return CastArgumentsToOldType(node, bindings, 0);

     }

     public override VCExpr VisitLeOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

       Contract.Requires((node != null));

       Contract.Ensures(Contract.Result<VCExpr>() != null);

-      return CastArguments(node, Type.Int, bindings, 0);

+      return CastArgumentsToOldType(node, bindings, 0);

     }

     public override VCExpr VisitGtOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

       Contract.Requires((node != null));

       Contract.Ensures(Contract.Result<VCExpr>() != null);

-      return CastArguments(node, Type.Int, bindings, 0);

+      return CastArgumentsToOldType(node, bindings, 0);

     }

     public override VCExpr VisitGeOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

       Contract.Requires((node != null));

       Contract.Ensures(Contract.Result<VCExpr>() != null);

-      return CastArguments(node, Type.Int, bindings, 0);

+      return CastArgumentsToOldType(node, bindings, 0);

     }

     public override VCExpr VisitSubtypeOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

@@ -1504,6 +1518,18 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Ensures(Contract.Result<VCExpr>() != null);

       return CastArguments(node, AxBuilder.U, bindings, 0);

     }

+    public override VCExpr VisitToIntOp(VCExprNAry node, VariableBindings bindings) {

+      Contract.Requires((bindings != null));

+      Contract.Requires((node != null));

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

+      return CastArgumentsToOldType(node, bindings, 0);

+    }

+    public override VCExpr VisitToRealOp(VCExprNAry node, VariableBindings bindings) {

+      Contract.Requires((bindings != null));

+      Contract.Requires((node != null));

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

+      return CastArgumentsToOldType(node, bindings, 0);

+    }

     public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) {

       Contract.Requires((bindings != null));

       Contract.Requires((node != null));

diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 38541881..fcfd0041 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -49,6 +49,12 @@ namespace Microsoft.Boogie {
       return new VCExprIntLit(x);

     }

 

+    public VCExpr/*!*/ Real(BigDec x) {

+      Contract.Ensures(Contract.Result<VCExpr>() != null);

+

+      return new VCExprRealLit(x);

+    }

+

     public VCExpr/*!*/ Function(VCExprOp/*!*/ op,

                             List<VCExpr/*!*/>/*!*/ arguments,

                             List<Type/*!*/>/*!*/ typeArguments) {

@@ -199,7 +205,8 @@ namespace Microsoft.Boogie {
         Contract.Requires(e1 != null);

         Contract.Ensures(Contract.Result<VCExpr>() != null);

 

-        return Function(AddOp, e0, e1);

+        VCExprOp op = cce.NonNull(cce.NonNull(e0).Type).IsInt ? AddIOp : AddROp;

+        return Function(op, e0, e1);

     }

     public VCExpr/*!*/ Or(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {

       Contract.Requires(e0 != null);

@@ -308,11 +315,16 @@ namespace Microsoft.Boogie {
     ////////////////////////////////////////////////////////////////////////////////

     // Further operators

 

-    public static readonly VCExprOp AddOp = new VCExprNAryOp(2, Type.Int);

-    public static readonly VCExprOp SubOp = new VCExprNAryOp(2, Type.Int);

-    public static readonly VCExprOp MulOp = new VCExprNAryOp(2, Type.Int);

-    public static readonly VCExprOp DivOp = new VCExprNAryOp(2, Type.Int);

+    public static readonly VCExprOp AddIOp = new VCExprNAryOp(2, Type.Int);

+    public static readonly VCExprOp AddROp = new VCExprNAryOp(2, Type.Real);

+    public static readonly VCExprOp SubIOp = new VCExprNAryOp(2, Type.Int);

+    public static readonly VCExprOp SubROp = new VCExprNAryOp(2, Type.Real);

+    public static readonly VCExprOp MulIOp = new VCExprNAryOp(2, Type.Int);

+    public static readonly VCExprOp MulROp = new VCExprNAryOp(2, Type.Real);

+    public static readonly VCExprOp DivIOp = new VCExprNAryOp(2, Type.Int);

+    public static readonly VCExprOp DivROp = new VCExprNAryOp(2, Type.Real);

     public static readonly VCExprOp ModOp = new VCExprNAryOp(2, Type.Int);

+    public static readonly VCExprOp PowOp = new VCExprNAryOp(2, Type.Real);

     public static readonly VCExprOp LtOp = new VCExprNAryOp(2, Type.Bool);

     public static readonly VCExprOp LeOp = new VCExprNAryOp(2, Type.Bool);

     public static readonly VCExprOp GtOp = new VCExprNAryOp(2, Type.Bool);

@@ -322,6 +334,8 @@ namespace Microsoft.Boogie {
     // the type of the compared terms

     public static readonly VCExprOp Subtype3Op = new VCExprNAryOp(3, Type.Bool);

     public static readonly VCExprOp IfThenElseOp = new VCExprIfThenElseOp();

+    public static readonly VCExprOp ToIntOp = new VCExprNAryOp(1, Type.Int);

+    public static readonly VCExprOp ToRealOp = new VCExprNAryOp(1, Type.Real);

 

     public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);

 

@@ -376,13 +390,17 @@ namespace Microsoft.Boogie {
       MulOp,

       DivOp,

       ModOp,

+      RealDivOp,

+      PowOp,

       LtOp,

       LeOp,

       GtOp,

       GeOp,

       SubtypeOp,

       Subtype3Op,

-      BvConcatOp

+      BvConcatOp,

+      ToIntOp,

+      ToRealOp

     };

     internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict;

     [ContractInvariantMethod]

@@ -399,17 +417,24 @@ namespace Microsoft.Boogie {
       SingletonOpDict.Add(AndOp, SingletonOp.AndOp);

       SingletonOpDict.Add(OrOp, SingletonOp.OrOp);

       SingletonOpDict.Add(ImpliesOp, SingletonOp.ImpliesOp);

-      SingletonOpDict.Add(AddOp, SingletonOp.AddOp);

-      SingletonOpDict.Add(SubOp, SingletonOp.SubOp);

-      SingletonOpDict.Add(MulOp, SingletonOp.MulOp);

-      SingletonOpDict.Add(DivOp, SingletonOp.DivOp);

+      SingletonOpDict.Add(AddIOp, SingletonOp.AddOp);

+      SingletonOpDict.Add(AddROp, SingletonOp.AddOp);

+      SingletonOpDict.Add(SubIOp, SingletonOp.SubOp);

+      SingletonOpDict.Add(SubROp, SingletonOp.SubOp);

+      SingletonOpDict.Add(MulIOp, SingletonOp.MulOp);

+      SingletonOpDict.Add(MulROp, SingletonOp.MulOp);

+      SingletonOpDict.Add(DivIOp, SingletonOp.DivOp);

+      SingletonOpDict.Add(DivROp, SingletonOp.RealDivOp);

       SingletonOpDict.Add(ModOp, SingletonOp.ModOp);

+      SingletonOpDict.Add(PowOp, SingletonOp.PowOp);

       SingletonOpDict.Add(LtOp, SingletonOp.LtOp);

       SingletonOpDict.Add(LeOp, SingletonOp.LeOp);

       SingletonOpDict.Add(GtOp, SingletonOp.GtOp);

       SingletonOpDict.Add(GeOp, SingletonOp.GeOp);

       SingletonOpDict.Add(SubtypeOp, SingletonOp.SubtypeOp);

       SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op);

+      SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp);

+      SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp);

     }

 

     ////////////////////////////////////////////////////////////////////////////////

@@ -810,6 +835,27 @@ namespace Microsoft.Boogie.VCExprAST {
     }

   }

 

+  public class VCExprRealLit : VCExprLiteral {

+    public readonly BigDec Val;

+    internal VCExprRealLit(BigDec val)

+      : base(Type.Real) {

+      this.Val = val;

+    }

+    [Pure]

+    [Reads(ReadsAttribute.Reads.Nothing)]

+    public override bool Equals(object that) {

+      if (Object.ReferenceEquals(this, that))

+        return true;

+      if (that is VCExprRealLit)

+        return Val == ((VCExprRealLit)that).Val;

+      return false;

+    }

+    [Pure]

+    public override int GetHashCode() {

+      return Val.GetHashCode() * 72321;

+    }

+  }

+

   /////////////////////////////////////////////////////////////////////////////////

   // Operator expressions with fixed arity

   [ContractClassFor(typeof(VCExprNAry))]

@@ -1218,6 +1264,10 @@ namespace Microsoft.Boogie.VCExprAST {
             return visitor.VisitDivOp(expr, arg);

           case VCExpressionGenerator.SingletonOp.ModOp:

             return visitor.VisitModOp(expr, arg);

+          case VCExpressionGenerator.SingletonOp.RealDivOp:

+            return visitor.VisitRealDivOp(expr, arg);

+          case VCExpressionGenerator.SingletonOp.PowOp:

+            return visitor.VisitPowOp(expr, arg);

           case VCExpressionGenerator.SingletonOp.LtOp:

             return visitor.VisitLtOp(expr, arg);

           case VCExpressionGenerator.SingletonOp.LeOp:

@@ -1232,6 +1282,10 @@ namespace Microsoft.Boogie.VCExprAST {
             return visitor.VisitSubtype3Op(expr, arg);

           case VCExpressionGenerator.SingletonOp.BvConcatOp:

             return visitor.VisitBvConcatOp(expr, arg);

+          case VCExpressionGenerator.SingletonOp.ToIntOp:

+            return visitor.VisitToIntOp(expr, arg);

+          case VCExpressionGenerator.SingletonOp.ToRealOp:

+            return visitor.VisitToRealOp(expr, arg);

           default:

             Contract.Assert(false);

             throw new cce.UnreachableException();

diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index adb3b27e..00e6fb9c 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -290,12 +290,22 @@ namespace Microsoft.Boogie.VCExprAST {
     public bool VisitDivOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

       //Contract.Requires(node != null);

-      return PrintNAry("/", node, wr);

+      return PrintNAry("div", node, wr);

     }

     public bool VisitModOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

       //Contract.Requires(node != null);

-      return PrintNAry("%", node, wr);

+      return PrintNAry("mod", node, wr);

+    }

+    public bool VisitRealDivOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      return PrintNAry("/", node, wr);

+    }

+    public bool VisitPowOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      return PrintNAry("**", node, wr);

     }

     public bool VisitLtOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

@@ -327,6 +337,16 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return PrintNAry("<::", node, wr);

     }

+    public bool VisitToIntOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      return PrintNAry("int", node, wr);

+    }

+    public bool VisitToRealOp(VCExprNAry node, TextWriter wr) {

+      //Contract.Requires(wr != null);

+      //Contract.Requires(node != null);

+      return PrintNAry("real", node, wr);

+    }

     public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {

       //Contract.Requires(wr != null);

       //Contract.Requires(node != null);

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index 1a29bbeb..1dd1cac9 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -75,12 +75,16 @@ namespace Microsoft.Boogie.VCExprAST {
     Result VisitMulOp(VCExprNAry node, Arg arg);

     Result VisitDivOp(VCExprNAry node, Arg arg);

     Result VisitModOp(VCExprNAry node, Arg arg);

+    Result VisitRealDivOp(VCExprNAry node, Arg arg);

+    Result VisitPowOp(VCExprNAry node, Arg arg);

     Result VisitLtOp(VCExprNAry node, Arg arg);

     Result VisitLeOp(VCExprNAry node, Arg arg);

     Result VisitGtOp(VCExprNAry node, Arg arg);

     Result VisitGeOp(VCExprNAry node, Arg arg);

     Result VisitSubtypeOp(VCExprNAry node, Arg arg);

     Result VisitSubtype3Op(VCExprNAry node, Arg arg);

+    Result VisitToIntOp(VCExprNAry node, Arg arg);

+    Result VisitToRealOp(VCExprNAry node, Arg arg);

     Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg);

     Result VisitIfThenElseOp(VCExprNAry node, Arg arg);

     Result VisitCustomOp(VCExprNAry node, Arg arg);

@@ -179,6 +183,16 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();

     }

 

+    public Result VisitRealDivOp(VCExprNAry node, Arg arg) {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitPowOp(VCExprNAry node, Arg arg) {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

     public Result VisitLtOp(VCExprNAry node, Arg arg) {

       Contract.Requires(node != null);

       throw new NotImplementedException();

@@ -209,6 +223,16 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();

     }

 

+    public Result VisitToIntOp(VCExprNAry node, Arg arg) {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitToRealOp(VCExprNAry node, Arg arg) {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

     public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {

       Contract.Requires(node != null);

       throw new NotImplementedException();

@@ -1427,6 +1451,14 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return StandardResult(node, arg);

     }

+    public virtual Result VisitRealDivOp(VCExprNAry node, Arg arg) {

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitPowOp(VCExprNAry node, Arg arg) {

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

     public virtual Result VisitLtOp(VCExprNAry node, Arg arg) {

       //Contract.Requires(node != null);

       return StandardResult(node, arg);

@@ -1451,6 +1483,14 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return StandardResult(node, arg);

     }

+    public virtual Result VisitToIntOp(VCExprNAry node, Arg arg) {

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitToRealOp(VCExprNAry node, Arg arg) {

+      //Contract.Requires(node != null);

+      return StandardResult(node, arg);

+    }

     public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {

       //Contract.Requires(node != null);

       return StandardResult(node, arg);