mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-10-06 18:10:13 +01:00
commit a77694d9a8
2 changed files with 13 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/qe/qe.cpp
View file

@ -1451,10 +1451,15 @@ namespace qe {
if (assumption) m_solver.assert_expr(assumption); if (assumption) m_solver.assert_expr(assumption);
bool is_sat = false; bool is_sat = false;
lbool res = l_true; lbool res = l_true;
while (res == l_true) { while (true) {
res = m_solver.check(); res = m_solver.check();
if (res == l_true) is_sat = true; if (res == l_true) {
final_check(); is_sat = true;
final_check();
}
else {
break;
}
} }
if (res == l_undef) { if (res == l_undef) {
free_vars.append(num_vars, vars); free_vars.append(num_vars, vars);

9
src/util/stopwatch.h
View file

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