diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/statistics.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index 9273f2167..04078ef50 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -112,8 +112,8 @@ void StatisticsBase::flushInformation(std::ostream &out) const { out << d_prefix << s_regDelim; } s->flushStat(out); - out << std::endl; } + out << std::endl; #endif /* CVC4_STATISTICS_ON */ } @@ -126,8 +126,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 */ } |