From 4ee0462beb5c46747854cf73cfa2f67af22496ff Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 15:43:33 -0700
Subject: [PATCH] fix #3590

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/solver/parallel_tactic.cpp | 6 ++++++
 src/tactic/tactic.cpp          | 2 +-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index 34d20b843..cf4a5389c 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -33,6 +33,7 @@ Notes:
 #include <cmath>
 #include <condition_variable>
 #include "util/scoped_ptr_vector.h"
+#include "ast/ast_pp.h"
 #include "ast/ast_util.h"
 #include "ast/ast_translation.h"
 #include "solver/solver.h"
@@ -141,6 +142,8 @@ class parallel_tactic : public tactic {
             for (auto* t : m_active) dealloc(t);
             m_tasks.reset();
             m_active.reset();
+            m_num_waiters = 0;
+            m_shutdown = false;
         }
 
         std::ostream& display(std::ostream& out) {
@@ -696,6 +699,7 @@ public:
     }
 
     void operator ()(const goal_ref & g,goal_ref_buffer & result) override {
+        cleanup();
         fail_if_proof_generation("parallel-tactic", g);
         ast_manager& m = g->m();        
         solver* s = m_solver->translate(m, m_params);
@@ -744,6 +748,8 @@ public:
 
     void cleanup() override {
         m_queue.reset();
+        m_models.reset();
+        m_stats.reset();
     }
 
     tactic* translate(ast_manager& m) override {
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 32197107b..b5c5025fa 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -178,7 +178,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
 
     if (r.size() > 0) {
         pr = r[0]->pr(0);
-        TRACE("tactic", tout << pr << "\n";);
+        CTRACE("tactic", pr, tout << pr << "\n";);
     }