From bb5395b35dcea5078c9b38a2f091f26256faac34 Mon Sep 17 00:00:00 2001
From: Dietrich <dgeisler50@gmail.com>
Date: Mon, 20 Jul 2015 22:27:32 -0600
Subject: Float type now works correctly for simple variable declaration and
 comparison.

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

(limited to 'Source/Provers')

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index c7ae9d57..3633a9c0 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 t.ToString(); //TODO: Match z3 syntax
+        return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")"; //TODO: Match z3 syntax
       else if (t.IsBv) {
         return "(_ BitVec " + t.BvBits + ")";
       } else {
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 2b09362b..4a1331c5 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -93,7 +93,6 @@ 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