From 2f33bafd5a7696a57a04555bc6521063f069ef59 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Thu, 21 Feb 2019 14:59:31 +0000
Subject: [PATCH] stopwatches: fix a few places that would call start/stop
 multiple times

---
 src/muz/rel/dl_instruction.cpp | 11 +++++------
 src/sat/sat_local_search.cpp   |  1 -
 src/smt/smt_context.cpp        |  1 -
 src/util/timer.h               |  2 +-
 4 files changed, 6 insertions(+), 9 deletions(-)

diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index 2b76d99f7..79508a4f6 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/src/muz/rel/dl_instruction.cpp
@@ -41,7 +41,6 @@ namespace datalog {
 
     execution_context::~execution_context() {
         reset();
-        dealloc(m_stopwatch);
     }
 
     void execution_context::reset() {
@@ -104,15 +103,15 @@ namespace datalog {
         m_timelimit_ms = time_in_ms;
         if (!m_stopwatch) {
             m_stopwatch = alloc(stopwatch);
+        } else {
+            m_stopwatch->stop();
+            m_stopwatch->reset();
         }
-        m_stopwatch->stop();
-        m_stopwatch->reset();
         m_stopwatch->start();
     }
     void execution_context::reset_timelimit() {
-        if (m_stopwatch) {
-            m_stopwatch->stop();
-        }
+        dealloc(m_stopwatch);
+        m_stopwatch = nullptr;
         m_timelimit_ms = 0;
     }
 
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 7c3ebb688..cdb90e2a0 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -515,7 +515,6 @@ namespace sat {
         reinit();
         DEBUG_CODE(verify_slack(););
         timer timer;
-        timer.start();
         unsigned step = 0, total_flips = 0, tries = 0;
         
         for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 86b3374fc..ecb69b418 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3496,7 +3496,6 @@ namespace smt {
         m_case_split_queue             ->init_search_eh();
         m_next_progress_sample         = 0;
         TRACE("literal_occ", display_literal_num_occs(tout););
-        m_timer.start();
     }
 
     void context::end_search() {
diff --git a/src/util/timer.h b/src/util/timer.h
index 37566e613..e2ddb55e7 100644
--- a/src/util/timer.h
+++ b/src/util/timer.h
@@ -27,7 +27,7 @@ Revision History:
 class timer {
     stopwatch m_watch;
 public:
-    void start() {
+    timer() {
         m_watch.start();
     }