diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-24 18:37:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-24 18:37:22 +0000 |
commit | 1f48835b7252757bb778a93bdac2d62e1dea59bc (patch) | |
tree | 1b2f2cda4091a146a2ddfbfcf137459e712fcc17 /src/util/statistics_registry.h | |
parent | e2611a54c5479086df0c4a80f56597aae80b5c4e (diff) |
Fix the memout issue seen in recent nightly regressions (was due to a
Statistics-printing problem, limited to certain benchmarks).
Mark some unlabeled header files "cvc4_private.h".
Other minor cleanup.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/util/statistics_registry.h')
-rw-r--r-- | src/util/statistics_registry.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index b2180ab59..870a88d66 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -148,7 +148,7 @@ template <> inline SExpr mkSExpr(const double& x) { // roundabout way to get a Rational from a double std::stringstream ss; - ss << std::fixed << x; + ss << std::fixed << std::setprecision(8) << x; return Rational::fromDecimal(ss.str()); } @@ -487,7 +487,7 @@ public: SExpr getValue() const { std::stringstream ss; - ss << d_data; + ss << std::fixed << std::setprecision(8) << d_data; return SExpr(Rational::fromDecimal(ss.str())); } @@ -769,7 +769,7 @@ public: SExpr getValue() const { std::stringstream ss; - ss << std::fixed << d_data; + ss << std::fixed << std::setprecision(8) << d_data; return SExpr(Rational::fromDecimal(ss.str())); } |