From 52aa9b8f63a3d955031e7a0dfd6e575ca7cf76b3 Mon Sep 17 00:00:00 2001
From: Dietrich <dgeisler50@gmail.com>
Date: Mon, 13 Jul 2015 19:40:09 -0600
Subject: Modified internal abstract float representation to allow user-defined
 mantissa and exponent

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 4 ++--
 Source/Provers/SMTLib/SMTLibProcess.cs    | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'Source/Provers')

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index b834aa6b..c7ae9d57 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -141,7 +141,7 @@ namespace Microsoft.Boogie.SMTLib
       else if (t.IsReal)
         return "Real";
       else if (t.IsFloat)
-        return "Real"; //TODO: Make to be a float
+        return t.ToString(); //TODO: Match z3 syntax
       else if (t.IsBv) {
         return "(_ BitVec " + t.BvBits + ")";
       } else {
@@ -690,7 +690,7 @@ namespace Microsoft.Boogie.SMTLib
       }
 
       public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
-      {
+      { //TODO: match z3
         WriteApplication("/f", node, options);
         return true;
       }
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 4a1331c5..2b09362b 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -93,6 +93,7 @@ namespace Microsoft.Boogie.SMTLib
         log = log.Replace("\r", "").Replace("\n", " ");
         Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
       }
+      Console.WriteLine(cmd); //TODO: Remove This Line
       toProver.WriteLine(cmd);
     }
 
-- 
cgit v1.2.3