diff options
| author | Tim King <taking@cs.nyu.edu> | 2018-02-02 17:03:10 -0800 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-02 19:03:10 -0600 |
| commit | 1b24f3f0fd5fdd4163a46689949fa8a5c60f3322 (patch) | |
| tree | d312cd6b42f002a4545e819bb097ada72d6249e0 /src/main/command_executor.cpp | |
| parent | ae5c1a5c3a9c6eb7d1af1a4ddbcb841cf7ce4c70 (diff) | |
Restoring ostream format. Resolves a few CIDs 1362780. (#1543)
Diffstat (limited to 'src/main/command_executor.cpp')
| -rw-r--r-- | src/main/command_executor.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 7c8ee7827..a7666dfcf 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -193,7 +193,10 @@ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out) return !cmd->fail(); } -void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString) { +void printStatsIncremental(std::ostream& out, + const std::string& prvsStatsString, + const std::string& curStatsString) +{ if(prvsStatsString == "") { out << curStatsString; return; @@ -229,9 +232,11 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString (std::istringstream(curStatValue) >> curFloat); if(isFloat) { + const std::streamsize old_precision = out.precision(); out << curStatName << ", " << curStatValue << " " << "(" << std::setprecision(8) << (curFloat-prvsFloat) << ")" << std::endl; + out.precision(old_precision); } else { out << curStatName << ", " << curStatValue << std::endl; } |