1 files changed, 5 insertions, 18 deletions
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 6f7f5c485..d824e0f21 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -23,8 +23,6 @@
 
 namespace CVC4 {
 
-std::string StatisticsBase::s_regDelim("::");
-
 bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const {
   return s1->getName() < s2->getName();
 }
@@ -34,17 +32,14 @@ StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const
 }
 
 StatisticsBase::StatisticsBase() :
-  d_prefix(),
   d_stats() {
 }
 
 StatisticsBase::StatisticsBase(const StatisticsBase& stats) :
-  d_prefix(stats.d_prefix),
   d_stats() {
 }
 
 StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) {
-  d_prefix = stats.d_prefix;
   return *this;
 }
 
@@ -106,10 +101,8 @@ void StatisticsBase::flushInformation(std::ostream &out) const {
       i != d_stats.end();
       ++i) {
     Stat* s = *i;
-    if(d_prefix != "") {
-      out << d_prefix << s_regDelim;
-    }
-    s->flushStat(out);
+    out << s->getName() << ", ";
+    s->flushInformation(out);
     out << std::endl;
   }
 #endif /* CVC4_STATISTICS_ON */
@@ -119,11 +112,9 @@ void StatisticsBase::safeFlushInformation(int fd) const {
 #ifdef CVC4_STATISTICS_ON
   for (StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
     Stat* s = *i;
-    if (d_prefix.size() != 0) {
-      safe_print(fd, d_prefix);
-      safe_print(fd, s_regDelim);
-    }
-    s->safeFlushStat(fd);
+    safe_print(fd, s->getName());
+    safe_print(fd, ", ");
+    s->safeFlushInformation(fd);
     safe_print(fd, "\n");
   }
 #endif /* CVC4_STATISTICS_ON */
@@ -140,8 +131,4 @@ SExpr StatisticsBase::getStatistic(std::string name) const {
   }
 }
 
-void StatisticsBase::setPrefix(const std::string& prefix) {
-  d_prefix = prefix;
-}
-
 }/* CVC4 namespace */