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

diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index e5bb6e532e60b3a0bab36687912a64183a2843bd..d078473adb7a267e8abcaab875d399cae1d8c0eb 100644 (file)
--- 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 de647bad614d32019b9439af35f419301d2a575e..b000e91e8240f5b6ac9a5dd54e48f5a77b6d15bd 100644 (file)
--- 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