From 63c1c22c3c47629740358bc8dbcedcdaac339a6f Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 7 Aug 2018 13:18:44 -0700
Subject: [PATCH] Make output of flushInformation and safeFlushInformation
 consistent. (#2280)

---
 src/util/statistics.cpp        | 1 +
 src/util/statistics_registry.h | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

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
-- 
2.30.2