mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Fix for bogus runtime reports on Linux. Thanks to Vladimir Klebanov for reporting this one.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-10-06 18:06:36 +01:00
parent 7ef1e8a3de
commit 929880e4fd
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/util/stopwatch.h
View file

@ -105,7 +105,7 @@ public:
mach_timespec_t _stop;
clock_get_time(m_host_clock, &_stop);
m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull;
m_time += (_stop.tv_nsec - m_start.tv_nsec);
m_time += (_stop.tv_nsec - m_start.tv_nsec);
m_running = false;
}
}
@ -146,7 +146,7 @@ public:
void start() {
if (!m_running) {
clock_gettime(CLOCK_THREAD_CPUTIME_ID, &m_start);
clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &m_start);
m_running = true;
}
}
@ -154,9 +154,10 @@ public:
void stop() {
if (m_running) {
struct timespec _stop;
clock_gettime(CLOCK_THREAD_CPUTIME_ID, &_stop);
clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &_stop);
m_time += (_stop.tv_sec - m_start.tv_sec) * 1000000000ull;
m_time += (_stop.tv_nsec - m_start.tv_nsec);
if (m_time != 0 || _stop.tv_nsec >= m_start.tv_nsec)
m_time += (_stop.tv_nsec - m_start.tv_nsec);
m_running = false;
}
}