1 files changed, 80 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 06aa5bbe..7b2525f7 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -121,7 +121,7 @@ namespace Microsoft.Boogie.SMTLib
           }
           sb.Append(']');
           TypeToStringHelper(m.Result, sb);
-        } else if (t.IsBool || t.IsInt || t.IsReal || t.IsBv) {
+        } else if (t.IsBool || t.IsInt || t.IsReal || t.IsFloat || t.IsBv) {
           sb.Append(TypeToString(t));
         } else {
           System.IO.StringWriter buffer = new System.IO.StringWriter();
@@ -145,6 +145,8 @@ namespace Microsoft.Boogie.SMTLib
         return "Int";
       else if (t.IsReal)
         return "Real";
+      else if (t.IsFloat)
+        return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatSignificand + ")";
       else if (t.IsBv) {
         return "(_ BitVec " + t.BvBits + ")";
       } else {
@@ -204,6 +206,11 @@ namespace Microsoft.Boogie.SMTLib
         else
           wr.Write(lit.ToDecimalString());
       }
+      else if (node is VCExprFloatLit)
+      {
+        BigFloat lit = ((VCExprFloatLit)node).Val;
+        wr.Write("(" + lit.ToBVString() + ")");
+      }
       else {
         Contract.Assert(false);
         throw new cce.UnreachableException();
@@ -630,6 +637,78 @@ namespace Microsoft.Boogie.SMTLib
         return true;
       }
 
+      public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("fp.add RNE", node, options);
+        return true;
+      }
+
+      public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("fp.sub RNE", node, options);
+        return true;
+      }
+
+      public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("fp.mul RNE", node, options);
+        return true;
+      }
+
+      public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("fp.div RNE", node, options);
+        return true;
+      }
+
+      public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("fp.rem RNE", 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)
       {