Began adding the float type to VC expression

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;