diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/util/statistics_registry.cpp | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/util/statistics_registry.cpp')
-rw-r--r-- | src/util/statistics_registry.cpp | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 2ccbc2971..7f93a690e 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -20,8 +20,7 @@ #include <cstdlib> #include <iostream> -#include "base/cvc4_assert.h" -#include "base/cvc4_check.h" +#include "base/check.h" #include "lib/clock_gettime.h" #include "util/ostream_util.h" @@ -77,7 +76,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) { nsec -= nsec_per_sec; ++a.tv_sec; } - CVC4_DCHECK(nsec >= 0 && nsec < nsec_per_sec); + Assert(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } @@ -168,8 +167,8 @@ void StatisticsRegistry::registerStat(Stat* s) void StatisticsRegistry::unregisterStat(Stat* s) { #ifdef CVC4_STATISTICS_ON - CVC4_CHECK(s != nullptr); - CVC4_CHECK(d_stats.erase(s) > 0) + AlwaysAssert(s != nullptr); + AlwaysAssert(d_stats.erase(s) > 0) << "Statistic `" << s->getName() << "' was not registered with this registry."; #endif /* CVC4_STATISTICS_ON */ @@ -203,7 +202,7 @@ void TimerStat::start() { void TimerStat::stop() { if(CVC4_USE_STATISTICS) { - CVC4_CHECK(d_running) << "timer not running"; + AlwaysAssert(d_running) << "timer not running"; ::timespec end; clock_gettime(CLOCK_MONOTONIC, &end); d_data += end - d_start; |