From a76c0fbbfbb7e0e80c5d491da99fb6b56f408139 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Thu, 21 Feb 2019 11:49:41 +0000
Subject: [PATCH] simplify timeout mechanism and fix race conditions there

---
 src/shell/main.cpp   |  7 +++++--
 src/util/timeout.cpp | 26 ++++++++++----------------
 2 files changed, 15 insertions(+), 18 deletions(-)

diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index b036628b1..260cf8a79 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -115,6 +115,7 @@ void display_usage() {
 }
    
 void parse_cmd_line_args(int argc, char ** argv) {
+    long timeout = 0;
     int i = 1;
     char * eq_pos = nullptr;
     while (i < argc) {
@@ -216,8 +217,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
             else if (strcmp(opt_name, "T") == 0) {
                 if (!opt_arg)
                     error("option argument (-T:timeout) is missing.");
-                long tm = strtol(opt_arg, nullptr, 10);
-                set_timeout(tm * 1000);
+                timeout = strtol(opt_arg, nullptr, 10);
             }
             else if (strcmp(opt_name, "t") == 0) {
                 if (!opt_arg)
@@ -292,6 +292,9 @@ void parse_cmd_line_args(int argc, char ** argv) {
         }
         i++;
     }
+
+    if (timeout)
+        set_timeout(timeout * 1000);
 }
 
 
diff --git a/src/util/timeout.cpp b/src/util/timeout.cpp
index ad02a747d..1a92ae867 100644
--- a/src/util/timeout.cpp
+++ b/src/util/timeout.cpp
@@ -19,7 +19,6 @@ Revision History:
 
 --*/
 #include<iostream>
-#include "util/z3_omp.h"
 #include "util/util.h"
 #include "util/timeout.h"
 #include "util/error_codes.h"
@@ -34,26 +33,21 @@ namespace {
 class g_timeout_eh : public event_handler {
 public:
     void operator()(event_handler_caller_t caller_id) override {
-        #pragma omp critical (g_timeout_cs) 
-        {
-            std::cout << "timeout\n";
-            m_caller_id = caller_id;
-            if (g_on_timeout)
-                g_on_timeout();
-            if (g_timeout) 
-                delete g_timeout;
-            g_timeout = nullptr;
-            throw z3_error(ERR_TIMEOUT);
-        }
+        std::cout << "timeout\n";
+        m_caller_id = caller_id;
+        if (g_on_timeout)
+            g_on_timeout();
+        throw z3_error(ERR_TIMEOUT);
     }
 };
 }
 
-void set_timeout(long ms) {
-    if (g_timeout) 
-        delete g_timeout;
+static g_timeout_eh eh;
 
-    g_timeout = new scoped_timer(ms, new g_timeout_eh());
+void set_timeout(long ms) {
+    SASSERT(!g_timeout);
+    // this is leaked, but since it's only used in the shell, it's ok
+    g_timeout = new scoped_timer(ms, &eh);
 }
 
 void register_on_timeout_proc(void (*proc)()) {