From 0de31496344e69e5cbb0b1310818ea76425ddbf8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 29 Oct 2020 11:15:07 -0700
Subject: [PATCH] fix #4763

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/scoped_timer.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index c8273b3bf..14b38b56f 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -118,8 +118,8 @@ scoped_timer::~scoped_timer() {
 
 void scoped_timer::finalize() {
     unsigned deleted = 0;
-
-    while (deleted < num_workers) {
+    unsigned tries = 0;
+    while (deleted < num_workers && tries < 10) {
         workers.lock();
         for (auto w : available_workers) {
             w->work = 2;
@@ -135,5 +135,6 @@ void scoped_timer::finalize() {
             delete w->m_thread;
             delete w;
         }
+        ++tries;
     }
 }