From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 7 Aug 2018 20:18:44 +0000 (-0700)
Subject: Make output of flushInformation and safeFlushInformation consistent. (#2280)
X-Git-Tag: cvc5-1.0.0~4808
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=63c1c22c3c47629740358bc8dbcedcdaac339a6f;p=cvc5.git

Make output of flushInformation and safeFlushInformation consistent. (#2280)
---

diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index e5bb6e532..d078473ad 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -112,6 +112,7 @@ void StatisticsBase::flushInformation(std::ostream &out) const {
       out << d_prefix << s_regDelim;
     }
     s->flushStat(out);
+    out << std::endl;
   }
 #endif /* CVC4_STATISTICS_ON */
 }
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index de647bad6..b000e91e8 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -562,7 +562,7 @@ public:
 
   void flushInformation(std::ostream& out) const override
   {
-    out << d_data << std::endl;
+    out << d_data;
   }
 
   void safeFlushInformation(int fd) const override