From: Tim King Date: Tue, 7 Nov 2017 23:37:31 +0000 (-0800) Subject: Initialize TimerStat::d_start. (#1330) X-Git-Tag: cvc5-1.0.0~5498 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5a98219512880392bc045f21a3c857438cd76506;p=cvc5.git Initialize TimerStat::d_start. (#1330) * Initialize TimerStat::d_start. * 0 initializing d_data. --- diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 6e74357c6..3de001e32 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -720,13 +720,8 @@ public: * Construct a timer statistic with the given name. Newly-constructed * timers have a 0.0 value and are not running. */ - TimerStat(const std::string& name) : - BackedStat< timespec >(name, timespec()), - d_running(false) { - /* timespec is POD and so may not be initialized to zero; - * here, ensure it is */ - d_data.tv_sec = d_data.tv_nsec = 0; - } + TimerStat(const std::string& name) + : BackedStat(name, {0, 0}), d_start{0, 0}, d_running(false) {} /** Start the timer. */ void start();