From 6d8daacdecc84bafbb7c493aeeccfe5660d19d43 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Oct 2014 08:35:05 -0700 Subject: [PATCH 1/2] fix check for satisfiability before calling final_check Signed-off-by: Nikolaj Bjorner --- src/qe/qe.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index e573508bb..192d97c3b 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -1451,10 +1451,15 @@ namespace qe { if (assumption) m_solver.assert_expr(assumption); bool is_sat = false; lbool res = l_true; - while (res == l_true) { + while (true) { res = m_solver.check(); - if (res == l_true) is_sat = true; - final_check(); + if (res == l_true) { + is_sat = true; + final_check(); + } + else { + break; + } } if (res == l_undef) { free_vars.append(num_vars, vars); From 929880e4fd1f5f40955ba8caed7ed84eb5bd53a2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 6 Oct 2014 18:06:36 +0100 Subject: [PATCH 2/2] Fix for bogus runtime reports on Linux. Thanks to Vladimir Klebanov for reporting this one. --- src/util/stopwatch.h | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index 661d3762b..b2a397b6e 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -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; } }