diff options
| author |  Rustan Leino <unknown> | 2014-02-10 18:54:56 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-10 18:54:56 -0800 |
| commit | 7632fe2542f138a83ee3a9b39d5bcad09cd5fcf7 (patch) | |
| tree | 64f05c4a234fb3bfda727bd9f151b2dcd9a988d1 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
| parent | 8567d68f7f04f87b2d4270e18713bdcdf4d26031 (diff) | |
Fixed bug in printing real literals
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 1bea4633..1ccec455 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -195,9 +195,9 @@ namespace Microsoft.Boogie.SMTLib BigDec lit = ((VCExprRealLit)node).Val;
if (lit.IsNegative)
// In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")
- wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString(20));
+ wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());
else
- wr.Write(lit.ToDecimalString(20));
+ wr.Write(lit.ToDecimalString());
}
else {
Contract.Assert(false);
|