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);
diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h
index b9cf312b2..425a13567 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;
         }
     }