diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-08-03 05:59:23 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-03 07:59:23 -0500 |
| commit | b249f10578a078e032ed21bc7a3812b70d200c4d (patch) | |
| tree | c30aa14d5bcf41c0ba1f778dbe2fe3e26dcb086d | |
| parent | fc99192e73d6147fd6a87c7b6139a800173dd4c2 (diff) | |
Fix printing statistics in case of signals. (#2267)
| -rw-r--r-- | src/util/statistics.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index a6b20934c..e5bb6e532 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -113,7 +113,6 @@ void StatisticsBase::flushInformation(std::ostream &out) const { } s->flushStat(out); } - out << std::endl; #endif /* CVC4_STATISTICS_ON */ } @@ -126,8 +125,8 @@ void StatisticsBase::safeFlushInformation(int fd) const { safe_print(fd, s_regDelim); } s->safeFlushStat(fd); + safe_print(fd, "\n"); } - safe_print(fd, "\n"); #endif /* CVC4_STATISTICS_ON */ } |