Modified BigFloat to avoid evaluating the floating point value before sending it to z3

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;