1 files changed, 0 insertions, 12 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 3633a9c0..f030870e 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -689,12 +689,6 @@ namespace Microsoft.Boogie.SMTLib
         return true;
       }
 
-      public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
-      { //TODO: match z3
-        WriteApplication("/f", node, options);
-        return true;
-      }
-
       public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {
         WriteApplication("real_pow", node, options);
         return true;
@@ -746,12 +740,6 @@ 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;