2 files changed, 3 insertions, 2 deletions
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);
     }