diff options
| author |  Dietrich <dgeisler50@gmail.com> | 2015-07-20 22:27:32 -0600 |
|---|---|---|
| committer | Dietrich <dgeisler50@gmail.com> | 2015-07-20 22:27:32 -0600 |
| commit | bb5395b35dcea5078c9b38a2f091f26256faac34 (patch) | |
| tree | 5930116d3f65b25cdcd3a98cca6ced2e30f5e057 /Source/Provers | |
| parent | 52aa9b8f63a3d955031e7a0dfd6e575ca7cf76b3 (diff) | |
Float type now works correctly for simple variable declaration and comparison.
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProcess.cs | 1 |
2 files changed, 1 insertions, 2 deletions
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);
}
|