Modified translation so that z3 runs with type checking for simple binary operations

10 files changed, 567 insertions, 84 deletions

diff --git a/Source/Basetypes/BigFloat.cs b/Source/Basetypes/BigFloat.cs
index e9d5e670..9e798959 100644
--- a/Source/Basetypes/BigFloat.cs
+++ b/Source/Basetypes/BigFloat.cs
@@ -33,7 +33,7 @@ namespace Microsoft.Basetypes
     [Rep]

     internal readonly int exponentSize; //The bit size of the exponent

     [Rep]

-    internal readonly BigDec dec_value;

+    internal readonly String dec_value;

     [Rep]

     internal readonly bool isDec;

 

@@ -61,7 +61,7 @@ namespace Microsoft.Basetypes
       }

     }

 

-    public BigDec Decimal {

+    public String Decimal {

       get {

         return dec_value;

       }

@@ -102,7 +102,7 @@ namespace Microsoft.Basetypes
 

     public static BigFloat FromBigDec(BigDec v)

     {

-      return new BigFloat(v, 8, 24);

+      return new BigFloat(v.ToDecimalString(), 8, 24);

     }

 

     [Pure]

@@ -114,11 +114,11 @@ namespace Microsoft.Basetypes
       {

         switch (vals.Length) {

           case 1:

-            return new BigFloat(BigDec.FromString(vals[0]), 8, 24); 

+            return new BigFloat(vals[0], 8, 24); 

           case 2:

             return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), 8, 24);

           case 3:

-            return new BigFloat(BigDec.FromString(vals[0]), Int32.Parse(vals[1]), Int32.Parse(vals[2]));

+            return new BigFloat(vals[0], Int32.Parse(vals[1]), Int32.Parse(vals[2]));

           case 4:

             return new BigFloat(Int32.Parse(vals[0]), BIM.Parse(vals[1]), Int32.Parse(vals[2]), Int32.Parse(vals[3]));

           default:

@@ -136,10 +136,10 @@ namespace Microsoft.Basetypes
       this.mantissa = mantissa;

       this.mantissaSize = mantissaSize;

       this.isDec = false;

-      this.dec_value = BigDec.ZERO;

+      this.dec_value = "";

     }

 

-    internal BigFloat(BigDec dec_value, int exponentSize, int mantissaSize) {

+    internal BigFloat(String dec_value, int exponentSize, int mantissaSize) {

       this.exponentSize = exponentSize;

       this.mantissaSize = mantissaSize;

       this.exponent = 0;

@@ -181,7 +181,7 @@ namespace Microsoft.Basetypes
     [Pure]

     public override string/*!*/ ToString() {

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

-      return String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());

+      return isDec ? dec_value : String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());

     }

 

 

@@ -313,34 +313,8 @@ namespace Microsoft.Basetypes
 

     [Pure]

     public string ToDecimalString() {

-      //TODO: fix for fp functionality

-      string m = Mantissa.ToString();

-      var e = Exponent;

-      if (0 <= Exponent) {

-        return m + Zeros(e) + ".0";

-      } else {

-        e = -e;

-        // compute k to be the longest suffix of m consisting of all zeros (but no longer than e, and not the entire string)

-        var maxK = e < m.Length ? e : m.Length - 1;

-        var last = m.Length - 1;

-        var k = 0;

-        while (k < maxK && m[last - k] == '0') {

-          k++;

-        }

-        if (0 < k) {

-          // chop off the suffix of k zeros from m and adjust e accordingly

-          m = m.Substring(0, m.Length - k);

-          e -= k;

-        }

-        if (e == 0) {

-          return m;

-        } else if (e < m.Length) {

-          var n = m.Length - e;

-          return m.Substring(0, n) + "." + m.Substring(n);

-        } else {

-          return "0." + Zeros(e - m.Length) + m;

-        }

-      }

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

+      return isDec ? dec_value : String.Format("{0}x2^{1}", Mantissa.ToString(), Exponent.ToString());

     }

 

     [Pure]

@@ -436,7 +410,7 @@ namespace Microsoft.Basetypes
 

     public bool IsNegative {

       get {

-        return (isDec && dec_value >= BigDec.ZERO) || mantissa >= 0;

+        return (isDec && dec_value[0] == '-') || mantissa < 0;

       }

     }

 

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index cf6fb922..ad537288 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1642,7 +1642,6 @@ namespace Microsoft.Boogie {
           case Opcode.Div:

           case Opcode.Mod:

           case Opcode.RealDiv:

-          case Opcode.FloatDiv:

           case Opcode.Pow:

           case Opcode.Neq:  // Neq is allowed, but not Eq

           case Opcode.Subtype:

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index f030870e..629f7e2d 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -141,7 +141,7 @@ namespace Microsoft.Boogie.SMTLib
       else if (t.IsReal)

         return "Real";

       else if (t.IsFloat)

-        return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")"; //TODO: Match z3 syntax

+        return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")";

       else if (t.IsBv) {

         return "(_ BitVec " + t.BvBits + ")";

       } else {

@@ -204,11 +204,13 @@ namespace Microsoft.Boogie.SMTLib
       else if (node is VCExprFloatLit)

       {

         BigFloat lit = ((VCExprFloatLit)node).Val;

+        wr.Write(("((_ to_fp 8 24) roundTowardZero "));

         if (lit.IsNegative)

           // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")

           wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());

         else

           wr.Write(lit.ToDecimalString());

+        wr.Write(")");

       }

       else {

         Contract.Assert(false);

@@ -616,6 +618,78 @@ namespace Microsoft.Boogie.SMTLib
         return true;

       }

 

+      public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.add roundTowardZero", node, options);

+        return true;

+      }

+

+      public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.sub roundTowardZero", node, options);

+        return true;

+      }

+

+      public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.mul roundTowardZero", node, options);

+        return true;

+      }

+

+      public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.div roundTowardZero", node, options);

+        return true;

+      }

+

+      public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.rem roundTowardZero", node, options);

+        return true;

+      }

+

+      public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.min", node, options);

+        return true;

+      }

+

+      public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.max", node, options);

+        return true;

+      }

+

+      public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.leq", node, options);

+        return true;

+      }

+

+      public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.lt", node, options);

+        return true;

+      }

+

+      public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.geq", node, options);

+        return true;

+      }

+

+      public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.gt", node, options);

+        return true;

+      }

+

+      public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options)

+      {

+        WriteApplication("fp.eq", node, options);

+        return true;

+      }

+

       static char[] hex = { '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f' };

       public bool VisitBvOp(VCExprNAry node, LineariserOptions options)

       {

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 8e8b2d55..250e04c9 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -253,7 +253,7 @@ namespace Microsoft.Boogie.SMTLib
             //if (options.Inspector != null)

             //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");

 

-            options.AddWeakSmtOption("TYPE_CHECK", "false");

+            options.AddWeakSmtOption("TYPE_CHECK", "true");

             options.AddWeakSmtOption("smt.BV.REFLECT", "true");

 

             if (options.TimeLimit > 0)

@@ -334,7 +334,7 @@ namespace Microsoft.Boogie.SMTLib
             //if (options.Inspector != null)

             //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");

 

-            options.AddWeakSmtOption("TYPE_CHECK", "false");

+            options.AddWeakSmtOption("TYPE_CHECK", "true");

             options.AddWeakSmtOption("BV_REFLECT", "true");

 

             if (options.TimeLimit > 0)

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index f0dc505d..ad319c0e 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -1076,34 +1076,48 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Requires(cce.NonNullElements(args));

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

       Contract.Assert(args.Count == 2);

+      Type t = cce.NonNull(cce.NonNull(args[0]).Type);

 

       switch (app.Op) {

         case BinaryOperator.Opcode.Add:

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

+          if (t.IsInt) {

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

           }

-          else {

+          else if (t.IsReal) {

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

           }

+          else { //t is float

+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "+"), args);

+          }

         case BinaryOperator.Opcode.Sub:

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

+          if (t.IsInt) {

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

           }

-          else {

+          else if (t.IsReal) {

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

           }

+          else { //t is float

+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "-"), args);

+          }

         case BinaryOperator.Opcode.Mul:

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

+          if (t.IsInt) {

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

           }

-          else {

+          else if (t.IsReal) {

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

           }

+          else

+          { //t is float

+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "*"), args);

+          }

         case BinaryOperator.Opcode.Div:

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

         case BinaryOperator.Opcode.Mod:

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

         case BinaryOperator.Opcode.RealDiv:

+          if (t.IsFloat) {

+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "/"), args);

+          }

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

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

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

@@ -1118,16 +1132,26 @@ namespace Microsoft.Boogie.VCExprAST {
         case BinaryOperator.Opcode.Eq:

         case BinaryOperator.Opcode.Iff:

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

+          if (t.IsFloat)

+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "=="), args);

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

         case BinaryOperator.Opcode.Neq:

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

         case BinaryOperator.Opcode.Lt:

+          if (t.IsFloat)

+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "<"), args);

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

         case BinaryOperator.Opcode.Le:

+          if (t.IsFloat)

+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "<="), args);

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

         case BinaryOperator.Opcode.Ge:

+          if (t.IsFloat)

+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, ">="), args);

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

         case BinaryOperator.Opcode.Gt:

+          if (t.IsFloat)

+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, ">"), args);

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

         case BinaryOperator.Opcode.Imp:

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

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index 0ff6d67f..6f74fe08 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -384,6 +384,14 @@ namespace Microsoft.Boogie.VCExprAST {
     internal const string floatSubName = "floatSub";

     internal const string floatMulName = "floatMul";

     internal const string floatDivName = "floatDiv";

+    internal const string floatRemName = "floatRem";

+    internal const string floatMinName = "floatMin";

+    internal const string floatMaxName = "floatMax";

+    internal const string floatLeqName = "floatLeq";

+    internal const string floatLtName = "floatLt";

+    internal const string floatGeqName = "floatGeq";

+    internal const string floatGtName = "floatGt";

+    internal const string floatEqName = "floatEq";

     internal const string realPowName = "realPow";

     internal const string toIntName = "toIntCoercion";

     internal const string toRealName = "toRealCoercion";

@@ -888,7 +896,104 @@ namespace Microsoft.Boogie.VCExprAST {
         return true;

       }

 

-      public bool VisitBvOp(VCExprNAry node, LineariserOptions options) {

+      public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatAddName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatSubName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatMulName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatDivName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatRemName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatMinName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatMaxName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatLeqName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatLtName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatGeqName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatGtName, node, options);

+        return true;

+      }

+

+      public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

+        WriteTermApplication(floatEqName, node, options);

+        return true;

+      }

+

+      public bool VisitBvOp(VCExprNAry node, LineariserOptions options)

+      {

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

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

         WriteTermApplication("$make_bv" + node.Type.BvBits, node, options);

@@ -948,11 +1053,8 @@ namespace Microsoft.Boogie.VCExprAST {
             WriteTermApplication(intAddName, node, options);

           }

         }

-        else if (node.Type.IsReal) {

-          WriteTermApplication(realAddName, node, options);

-        }

         else {

-          WriteTermApplication(floatAddName, node, options);

+          WriteTermApplication(realAddName, node, options);

         }

         return true;

       }

@@ -1008,14 +1110,6 @@ namespace Microsoft.Boogie.VCExprAST {
         return true;

       }

 

-      public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)

-      {

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

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

-        WriteTermApplication(floatDivName, node, options);

-        return true;

-      }

-

       public bool VisitPowOp(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 5e821ea2..6fb38c27 100644
--- a/Source/VCExpr/TypeErasure.cs
+++ b/Source/VCExpr/TypeErasure.cs
@@ -1479,6 +1479,90 @@ namespace Microsoft.Boogie.TypeErasure {
       Contract.Ensures(Contract.Result<VCExpr>() != null);

       return CastArgumentsToOldType(node, bindings, 0);

     }

+    public override VCExpr VisitFloatAddOp(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 VisitFloatSubOp(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 VisitFloatMulOp(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 VisitFloatDivOp(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 VisitFloatRemOp(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 VisitFloatMinOp(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 VisitFloatMaxOp(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 VisitFloatLeqOp(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 VisitFloatLtOp(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 VisitFloatGeqOp(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 VisitFloatGtOp(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 VisitFloatEqOp(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 c44800fc..3f6e3b7a 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -324,7 +324,6 @@ namespace Microsoft.Boogie {
 

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

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

-    //public static readonly VCExprOp AddFOp = new VCExprNAryOp(2, Type.Float);

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

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

    // public static readonly VCExprOp SubFOp = new VCExprNAryOp(2, Type.Float);

@@ -359,11 +358,13 @@ namespace Microsoft.Boogie {
 

     // Float nodes

 

-    public VCExpr AddFOp(VCExpr f1, VCExpr f2)

+    public VCExprOp BinaryFloatOp(int exp, int man, string op)

     {

-      Contract.Requires(f1 != null);

-      Contract.Requires(f2 != null);

-      return Function(new VCExprFloatOp(f1.Type.FloatExponent, f1.Type.FloatMantissa));

+      Contract.Requires(exp > 0);

+      Contract.Requires(man > 0);

+      Contract.Requires(op != null);

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

+      return new VCExprBinaryFloatOp(exp, man, op);

     }

 

     // Bitvector nodes

@@ -441,7 +442,6 @@ namespace Microsoft.Boogie {
       SingletonOpDict.Add(ImpliesOp, SingletonOp.ImpliesOp);

       SingletonOpDict.Add(AddIOp, SingletonOp.AddOp);

       SingletonOpDict.Add(AddROp, SingletonOp.AddOp);

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

       SingletonOpDict.Add(SubIOp, SingletonOp.SubOp);

       SingletonOpDict.Add(SubROp, SingletonOp.SubOp);

       //SingletonOpDict.Add(SubFOp, SingletonOp.SubOp);

@@ -1677,18 +1677,19 @@ namespace Microsoft.Boogie.VCExprAST {
   /////////////////////////////////////////////////////////////////////////////////

   // Float operators

 

-  public class VCExprFloatOp : VCExprOp {

+  public class VCExprBinaryFloatOp : VCExprOp {

     public readonly int Mantissa;

     public readonly int Exponent;

+    private string op;

 

     public override int Arity {

       get {

-        return 1;

+        return 2;

       }

     }

     public override int TypeParamArity {

       get {

-        return 0;

+        return 2;

       }

     }

     public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {

@@ -1703,8 +1704,8 @@ namespace Microsoft.Boogie.VCExprAST {
     public override bool Equals(object that) {

       if (Object.ReferenceEquals(this, that))

         return true;

-      if (that is VCExprFloatOp)

-        return this.Exponent == ((VCExprFloatOp)that).Exponent && this.Mantissa == ((VCExprFloatOp)that).Mantissa;

+      if (that is VCExprBinaryFloatOp)

+        return this.Exponent == ((VCExprBinaryFloatOp)that).Exponent && this.Mantissa == ((VCExprBinaryFloatOp)that).Mantissa;

       return false;

     }

     [Pure]

@@ -1712,15 +1713,44 @@ namespace Microsoft.Boogie.VCExprAST {
       return Exponent * 81748912 + Mantissa * 67867979;

     }

 

-    internal VCExprFloatOp(int exp, int man) {

+    internal VCExprBinaryFloatOp(int exp, int man, string op) {

       this.Exponent = exp;

       this.Mantissa = man;

+      this.op = op;

     }

     public override Result Accept<Result, Arg>

            (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {

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

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

-      return visitor.VisitBvOp(expr, arg);

+      switch (op) { 

+      case ("+"):

+        return visitor.VisitFloatAddOp(expr, arg);

+      case ("-"):

+        return visitor.VisitFloatSubOp(expr, arg);

+      case ("*"):

+        return visitor.VisitFloatMulOp(expr, arg);

+      case ("/"):

+        return visitor.VisitFloatDivOp(expr, arg);

+      case ("rem"):

+        return visitor.VisitFloatRemOp(expr, arg);

+      case ("min"):

+        return visitor.VisitFloatMinOp(expr, arg);

+      case ("max"):

+        return visitor.VisitFloatMaxOp(expr, arg);

+      case ("<="):

+        return visitor.VisitFloatLeqOp(expr, arg);

+      case ("<"):

+        return visitor.VisitFloatLtOp(expr, arg);

+      case (">="):

+        return visitor.VisitFloatGeqOp(expr, arg);

+      case (">"):

+        return visitor.VisitFloatGtOp(expr, arg);

+      case ("=="):

+        return visitor.VisitFloatEqOp(expr, arg);

+      default:

+        Contract.Assert(false);

+        throw new cce.UnreachableException();

+      }

     }

   }

 

diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index 00e6fb9c..8e2f5d12 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -242,6 +242,78 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return PrintNAry("Store", node, wr);

     }

+    public bool VisitFloatAddOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.add", node, wr);

+    }

+    public bool VisitFloatSubOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.sub", node, wr);

+    }

+    public bool VisitFloatMulOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.mul", node, wr);

+    }

+    public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)

+    {

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

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

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

+    }

+    public bool VisitFloatRemOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.rem", node, wr);

+    }

+    public bool VisitFloatMinOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.min", node, wr);

+    }

+    public bool VisitFloatMaxOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.max", node, wr);

+    }

+    public bool VisitFloatLeqOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.leq", node, wr);

+    }

+    public bool VisitFloatLtOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.lt", node, wr);

+    }

+    public bool VisitFloatGeqOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.geq", node, wr);

+    }

+    public bool VisitFloatGtOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.gt", node, wr);

+    }

+    public bool VisitFloatEqOp(VCExprNAry node, TextWriter wr)

+    {

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

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

+      return PrintNAry("fp.eq", node, wr);

+    }

     public bool VisitBvOp(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 a1fb2ff4..c81f69e5 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -68,6 +68,18 @@ namespace Microsoft.Boogie.VCExprAST {
     Result VisitLabelOp(VCExprNAry node, Arg arg);

     Result VisitSelectOp(VCExprNAry node, Arg arg);

     Result VisitStoreOp(VCExprNAry node, Arg arg);

+    Result VisitFloatAddOp(VCExprNAry node, Arg arg);

+    Result VisitFloatSubOp(VCExprNAry node, Arg arg);

+    Result VisitFloatMulOp(VCExprNAry node, Arg arg);

+    Result VisitFloatDivOp(VCExprNAry node, Arg arg);

+    Result VisitFloatRemOp(VCExprNAry node, Arg arg);

+    Result VisitFloatMinOp(VCExprNAry node, Arg arg);

+    Result VisitFloatMaxOp(VCExprNAry node, Arg arg);

+    Result VisitFloatLeqOp(VCExprNAry node, Arg arg);

+    Result VisitFloatLtOp(VCExprNAry node, Arg arg);

+    Result VisitFloatGeqOp(VCExprNAry node, Arg arg);

+    Result VisitFloatGtOp(VCExprNAry node, Arg arg);

+    Result VisitFloatEqOp(VCExprNAry node, Arg arg);

     Result VisitBvOp(VCExprNAry node, Arg arg);

     Result VisitBvExtractOp(VCExprNAry node, Arg arg);

     Result VisitBvConcatOp(VCExprNAry node, Arg arg);

@@ -144,6 +156,78 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();

     }

 

+    public Result VisitFloatAddOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatSubOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatMulOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatDivOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatRemOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatMinOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatMaxOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatLeqOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatLtOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatGeqOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatGtOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

+    public Result VisitFloatEqOp(VCExprNAry node, Arg arg)

+    {

+      Contract.Requires(node != null);

+      throw new NotImplementedException();

+    }

+

     public Result VisitBvOp(VCExprNAry node, Arg arg) {

       Contract.Requires(node != null);

       throw new NotImplementedException();

@@ -189,12 +273,6 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();

     }

 

-    public Result VisitFloatDivOp(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();

@@ -1450,6 +1528,65 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return StandardResult(node, arg);

     }

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

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatSubOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatMulOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatDivOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatRemOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatMinOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatMaxOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatLeqOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatLtOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatGeqOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatGtOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

+    public virtual Result VisitFloatEqOp(VCExprNAry node, Arg arg)

+    {

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

+      return StandardResult(node, arg);

+    }

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

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

       return StandardResult(node, arg);

@@ -1494,11 +1631,6 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);

       return StandardResult(node, arg);

     }

-    public virtual Result VisitFloatDivOp(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);