diff options
| author | Tim King <taking@cs.nyu.edu> | 2018-02-09 12:34:47 -0800 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-09 14:34:47 -0600 |
| commit | a7f08481352ea1c45091b681e990ccc513ae175f (patch) | |
| tree | 76eabd2efdce313cde9aed1e9eb0be7e1c310b93 /src/util | |
| parent | d4b136c10ac3a226061d12cdf8e12340ad0a974d (diff) | |
Renaming CHECK to CVC4_CHECK. This avoids name collisions with other popular assertion macros. This name is likely temporary while Assert() is deprecated. (#1590)
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/statistics_registry.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 2dd1eddd7..b9f6998d4 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -77,7 +77,7 @@ inline timespec& operator-=(timespec& a, const timespec& b) { nsec -= nsec_per_sec; ++a.tv_sec; } - DCHECK(nsec >= 0 && nsec < nsec_per_sec); + CVC4_DCHECK(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } @@ -168,9 +168,10 @@ void StatisticsRegistry::registerStat(Stat* s) void StatisticsRegistry::unregisterStat(Stat* s) { #ifdef CVC4_STATISTICS_ON - CHECK(s != nullptr); - CHECK(d_stats.erase(s) > 0) << "Statistic `" << s->getName() - << "' was not registered with this registry."; + CVC4_CHECK(s != nullptr); + CVC4_CHECK(d_stats.erase(s) > 0) + << "Statistic `" << s->getName() + << "' was not registered with this registry."; #endif /* CVC4_STATISTICS_ON */ } /* StatisticsRegistry::unregisterStat() */ @@ -202,7 +203,7 @@ void TimerStat::start() { void TimerStat::stop() { if(__CVC4_USE_STATISTICS) { - CHECK(d_running) << "timer not running"; + CVC4_CHECK(d_running) << "timer not running"; ::timespec end; clock_gettime(CLOCK_MONOTONIC, &end); d_data += end - d_start; |