1 files changed, 12 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index f431c3d5..6accf79f 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -678,6 +678,12 @@ namespace Microsoft.Boogie.SMTLib
         return true;
       }
 
+      public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("/f", node, options);
+        return true;
+      }
+
       public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {
         WriteApplication("real_pow", node, options);
         return true;
@@ -729,6 +735,12 @@ namespace Microsoft.Boogie.SMTLib
         return true;
       }
 
+      public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options)
+      {
+        WriteApplication("to_float", node, options);
+        return true;
+      }
+
       private string ExtractDatatype(Function func) {
         if (func is DatatypeSelector) {
           DatatypeSelector selector = (DatatypeSelector) func;