From 904ab4bf9e1cf9f147218b88bbfd8ecc8b1a8a0e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 5 Sep 2014 11:18:34 -0700
Subject: [PATCH] address race condition in cleanup methods

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp              | 10 +++++++--
 src/solver/combined_solver.cpp               | 10 +++++++--
 src/solver/solver.h                          |  4 +++-
 src/solver/tactic2solver.cpp                 |  8 +++++--
 src/tactic/aig/aig.h                         |  2 --
 src/tactic/arith/add_bounds_tactic.cpp       | 10 ++-------
 src/tactic/arith/degree_shift_tactic.cpp     | 10 ++-------
 src/tactic/arith/diff_neq_tactic.cpp         | 13 +++--------
 src/tactic/arith/factor_tactic.cpp           | 10 ++-------
 src/tactic/arith/fix_dl_var_tactic.cpp       | 10 ++-------
 src/tactic/arith/fm_tactic.cpp               | 10 ++-------
 src/tactic/arith/lia2pb_tactic.cpp           | 10 ++-------
 src/tactic/arith/normalize_bounds_tactic.cpp |  9 ++------
 src/tactic/arith/pb2bv_tactic.cpp            |  9 ++------
 src/tactic/arith/propagate_ineqs_tactic.cpp  | 10 ++-------
 src/tactic/arith/recover_01_tactic.cpp       | 10 ++-------
 src/tactic/bv/bit_blaster_tactic.cpp         | 10 ++-------
 src/tactic/bv/bv1_blaster_tactic.cpp         | 10 ++-------
 src/tactic/bv/bv_size_reduction_tactic.cpp   | 10 ++-------
 src/tactic/bv/max_bv_sharing_tactic.cpp      | 10 ++-------
 src/tactic/core/cofactor_elim_term_ite.cpp   | 23 +++++++-------------
 src/tactic/core/cofactor_elim_term_ite.h     |  3 ++-
 src/tactic/core/ctx_simplify_tactic.cpp      |  9 ++------
 src/tactic/core/der_tactic.cpp               |  9 ++------
 src/tactic/core/elim_term_ite_tactic.cpp     |  9 ++------
 src/tactic/core/elim_uncnstr_tactic.cpp      | 11 +++-------
 src/tactic/core/occf_tactic.cpp              | 10 ++-------
 src/tactic/core/propagate_values_tactic.cpp  |  9 ++------
 src/tactic/core/reduce_args_tactic.cpp       | 11 +++-------
 src/tactic/core/simplify_tactic.cpp          |  9 ++------
 src/tactic/core/simplify_tactic.h            |  4 +++-
 src/tactic/core/solve_eqs_tactic.cpp         | 12 ++++------
 src/tactic/core/tseitin_cnf_tactic.cpp       | 12 +++-------
 src/tactic/fpa/fpa2bv_tactic.cpp             | 12 +++-------
 src/tactic/tactic.h                          |  8 ++++++-
 src/tactic/tactical.cpp                      | 16 +++++---------
 src/tactic/ufbv/macro_finder_tactic.cpp      |  9 ++------
 src/tactic/ufbv/quasi_macros_tactic.cpp      |  9 ++------
 src/tactic/ufbv/ufbv_rewriter_tactic.cpp     |  9 ++------
 39 files changed, 115 insertions(+), 264 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 20539266b..ce2838aba 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -346,8 +346,14 @@ cmd_context::~cmd_context() {
 }
 
 void cmd_context::set_cancel(bool f) {
-    if (m_solver)
-        m_solver->set_cancel(f);
+    if (m_solver) {
+        if (f) {
+            m_solver->cancel(); 
+        }
+        else {
+            m_solver->reset_cancel();
+        }
+    }
     if (has_manager())
         m().set_cancel(f);
 }
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index a98e5be49..dfbb62f65 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -218,8 +218,14 @@ public:
     }
 
     virtual void set_cancel(bool f) {
-        m_solver1->set_cancel(f);
-        m_solver2->set_cancel(f);
+        if (f) {
+            m_solver1->cancel();
+            m_solver2->cancel();
+        }
+        else {
+            m_solver1->reset_cancel();
+            m_solver2->reset_cancel();
+        }
     }
     
     virtual void set_progress_callback(progress_callback * callback) {
diff --git a/src/solver/solver.h b/src/solver/solver.h
index e047bace1..a95c649c0 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -99,7 +99,6 @@ public:
     */
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
 
-    virtual void set_cancel(bool f) {}
     /**
        \brief Interrupt this solver.
     */
@@ -130,6 +129,9 @@ public:
        \brief Display the content of this solver.
     */
     virtual void display(std::ostream & out) const;
+protected:
+    virtual void set_cancel(bool f) = 0;
+
 };
 
 #endif
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 1268fbcea..fb4898ecd 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -173,8 +173,12 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
 }
 
 void tactic2solver::set_cancel(bool f) {
-    if (m_tactic.get())
-        m_tactic->set_cancel(f);
+    if (m_tactic.get()) {
+        if (f) 
+            m_tactic->cancel();
+        else
+            m_tactic->reset_cancel();
+    }
 }
 
 void tactic2solver::collect_statistics(statistics & st) const {
diff --git a/src/tactic/aig/aig.h b/src/tactic/aig/aig.h
index c8befd9b2..291bfbcf3 100644
--- a/src/tactic/aig/aig.h
+++ b/src/tactic/aig/aig.h
@@ -73,8 +73,6 @@ public:
     void display(std::ostream & out, aig_ref const & r) const;
     void display_smt2(std::ostream & out, aig_ref const & r) const;
     unsigned get_num_aigs() const;
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
     void set_cancel(bool f);
 };
 
diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp
index d396359a3..9bf967be3 100644
--- a/src/tactic/arith/add_bounds_tactic.cpp
+++ b/src/tactic/arith/add_bounds_tactic.cpp
@@ -172,18 +172,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp
index a1aa0bdc8..e8fb72be4 100644
--- a/src/tactic/arith/degree_shift_tactic.cpp
+++ b/src/tactic/arith/degree_shift_tactic.cpp
@@ -319,18 +319,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
 protected:
diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp
index b534c8295..1a33bf4f2 100644
--- a/src/tactic/arith/diff_neq_tactic.cpp
+++ b/src/tactic/arith/diff_neq_tactic.cpp
@@ -398,20 +398,13 @@ public:
     }
     
     virtual void cleanup() {
-        unsigned num_conflicts = m_imp->m_num_conflicts;
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
+        d->m_num_conflicts = m_imp->m_num_conflicts;
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_conflicts = num_conflicts;
     }
 
 protected:
diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp
index 4eec83037..dc17a4f87 100644
--- a/src/tactic/arith/factor_tactic.cpp
+++ b/src/tactic/arith/factor_tactic.cpp
@@ -333,18 +333,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index d2e3ebf1f..693066ee1 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -338,18 +338,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index c4b7cbaf3..c180029ae 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -1682,18 +1682,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
     virtual void operator()(goal_ref const & in, 
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index 9ee8f6728..33d5f138e 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -345,18 +345,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp
index a62b311b5..323903f6c 100644
--- a/src/tactic/arith/normalize_bounds_tactic.cpp
+++ b/src/tactic/arith/normalize_bounds_tactic.cpp
@@ -191,17 +191,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 89195a9d5..643195b05 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -1002,17 +1002,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp
index 12954005f..d7e4f30d2 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.cpp
+++ b/src/tactic/arith/propagate_ineqs_tactic.cpp
@@ -548,16 +548,10 @@ void propagate_ineqs_tactic::set_cancel(bool f) {
 }
  
 void propagate_ineqs_tactic::cleanup() {
-    ast_manager & m = m_imp->m;
-    imp * d = m_imp;
+    imp * d = alloc(imp, m_imp->m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        d = m_imp;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel) 
-    {
-        m_imp = d;
-    }
 }
diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp
index 3b1a86345..3d222cf56 100644
--- a/src/tactic/arith/recover_01_tactic.cpp
+++ b/src/tactic/arith/recover_01_tactic.cpp
@@ -425,18 +425,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 0330141cb..33423c8b1 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -140,18 +140,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m(), m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
     unsigned get_num_steps() const {
diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp
index 8dcaf2112..5f20015ca 100644
--- a/src/tactic/bv/bv1_blaster_tactic.cpp
+++ b/src/tactic/bv/bv1_blaster_tactic.cpp
@@ -465,18 +465,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m(), m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
     
     unsigned get_num_steps() const {
diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index d3fdb6e56..e149afc75 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -392,17 +392,11 @@ void bv_size_reduction_tactic::set_cancel(bool f) {
 }
  
 void bv_size_reduction_tactic::cleanup() {
-    ast_manager & m = m_imp->m;
-    imp * d = m_imp;
+    imp * d = alloc(imp, m_imp->m);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp
index f60487d60..56b18dd8d 100644
--- a/src/tactic/bv/max_bv_sharing_tactic.cpp
+++ b/src/tactic/bv/max_bv_sharing_tactic.cpp
@@ -311,18 +311,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m(), m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp
index 1f560ef62..aca6d9084 100644
--- a/src/tactic/core/cofactor_elim_term_ite.cpp
+++ b/src/tactic/core/cofactor_elim_term_ite.cpp
@@ -683,12 +683,7 @@ cofactor_elim_term_ite::cofactor_elim_term_ite(ast_manager & m, params_ref const
 }
 
 cofactor_elim_term_ite::~cofactor_elim_term_ite() {
-    imp * d = m_imp;
-    #pragma omp critical (cofactor_elim_term_ite)
-    {
-        m_imp = 0;
-    }
-    dealloc(d);
+    dealloc(m_imp);
 }
 
 void cofactor_elim_term_ite::updt_params(params_ref const & p) {
@@ -704,19 +699,17 @@ void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
 }
     
 void cofactor_elim_term_ite::set_cancel(bool f) {
-    #pragma omp critical (cofactor_elim_term_ite)
-    {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
+    if (m_imp)
+        m_imp->set_cancel(f);
 }
 
 void cofactor_elim_term_ite::cleanup() {
-    ast_manager & m = m_imp->m;
-    #pragma omp critical (cofactor_elim_term_ite) 
+    ast_manager & m = m_imp->m;    
+    imp * d = alloc(imp, m, m_params);
+    #pragma omp critical (tactic_cancel)
     {
-        dealloc(m_imp);
-        m_imp = alloc(imp, m, m_params);
+        std::swap(d, m_imp);
     }
+    dealloc(d);
 }
 
diff --git a/src/tactic/core/cofactor_elim_term_ite.h b/src/tactic/core/cofactor_elim_term_ite.h
index ce2f31ea0..e734fcad6 100644
--- a/src/tactic/core/cofactor_elim_term_ite.h
+++ b/src/tactic/core/cofactor_elim_term_ite.h
@@ -37,8 +37,9 @@ public:
     
     void cancel() { set_cancel(true); }
     void reset_cancel() { set_cancel(false); }
-    void set_cancel(bool f);
     void cleanup();
+    void set_cancel(bool f);
+
 };
 
 #endif
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 71f4771a9..bb38d28ce 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -548,16 +548,11 @@ void ctx_simplify_tactic::set_cancel(bool f) {
 
 void ctx_simplify_tactic::cleanup() {
     ast_manager & m   = m_imp->m;
-    imp * d = m_imp;
+    imp * d = alloc(imp, m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp
index c2245b409..2277c3fa8 100644
--- a/src/tactic/core/der_tactic.cpp
+++ b/src/tactic/core/der_tactic.cpp
@@ -90,17 +90,12 @@ public:
 
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp
index 456bad5e0..e49884004 100644
--- a/src/tactic/core/elim_term_ite_tactic.cpp
+++ b/src/tactic/core/elim_term_ite_tactic.cpp
@@ -174,17 +174,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 4d64bf061..6d7bcb2f2 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -1036,18 +1036,13 @@ public:
     
     virtual void cleanup() {
         unsigned num_elim_apps = get_num_elim_apps();
-        ast_manager & m = m_imp->m_manager;
-        imp * d = m_imp;
+        ast_manager & m = m_imp->m_manager;        
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
         m_imp->m_num_elim_apps = num_elim_apps;
     }
 
diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp
index f8f6174b9..9b974ae19 100644
--- a/src/tactic/core/occf_tactic.cpp
+++ b/src/tactic/core/occf_tactic.cpp
@@ -225,18 +225,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
 protected:
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 1e358177f..5873efd61 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -255,17 +255,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
 protected:
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 59ed2dcd3..99375e6e8 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -541,17 +541,12 @@ void reduce_args_tactic::set_cancel(bool f) {
 }
 
 void reduce_args_tactic::cleanup() {
-    ast_manager & m   = m_imp->m();
-    imp * d = m_imp;
+    ast_manager & m   = m_imp->m();    
+    imp * d = alloc(imp, m);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index 95db962a7..39f10e10c 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -115,17 +115,12 @@ void simplify_tactic::set_cancel(bool f) {
 
 void simplify_tactic::cleanup() {
     ast_manager & m = m_imp->m();
-    imp * d = m_imp;
+    imp * d = alloc(imp, m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
 unsigned simplify_tactic::get_num_steps() const {
diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h
index fc9cb393c..1ba5a6da8 100644
--- a/src/tactic/core/simplify_tactic.h
+++ b/src/tactic/core/simplify_tactic.h
@@ -43,9 +43,11 @@ public:
     virtual void cleanup();
 
     unsigned get_num_steps() const;
-    virtual void set_cancel(bool f);
 
     virtual tactic * translate(ast_manager & m) { return alloc(simplify_tactic, m, m_params); }
+protected:
+    virtual void set_cancel(bool f);
+
 };
 
 tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 995940406..3b0a57d20 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -749,23 +749,19 @@ public:
     virtual void cleanup() {
         unsigned num_elim_vars = m_imp->m_num_eliminated_vars;
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
         expr_replacer * r = m_imp->m_r;
         if (r)
             r->set_substitution(0);
         bool owner = m_imp->m_r_owner;
         m_imp->m_r_owner  = false; // stole replacer
+
+        imp * d = alloc(imp, m, m_params, r, owner);
+        d->m_num_eliminated_vars = num_elim_vars;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params, r, owner);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_eliminated_vars = num_elim_vars;
     }
 
     virtual void collect_statistics(statistics & st) const {
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index b6c4b0655..c5be7ab1f 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -898,20 +898,14 @@ public:
     }
     
     virtual void cleanup() {
-        unsigned num_aux_vars = m_imp->m_num_aux_vars;
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
+        d->m_num_aux_vars = m_imp->m_num_aux_vars;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_aux_vars = num_aux_vars;
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index 3a6b7ea45..4a3a01b6f 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -138,19 +138,13 @@ public:
         (*m_imp)(in, result, mc, pc, core);
     }
     
-    virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+    virtual void cleanup() {        
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index 80de1bcd0..8b4f9f576 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -47,7 +47,6 @@ public:
 
     void cancel();
     void reset_cancel();
-    virtual void set_cancel(bool f) {}
     
     /**
        \brief Apply tactic to goal \c in.
@@ -96,6 +95,13 @@ public:
 
     // translate tactic to the given manager
     virtual tactic * translate(ast_manager & m) = 0;
+private:
+    friend class nary_tactical;
+    friend class binary_tactical;
+    friend class unary_tactical;
+
+    virtual void set_cancel(bool f) {}
+
 };
 
 typedef ref<tactic>         tactic_ref;
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index ca66b7a14..1e0b07e9d 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -102,11 +102,8 @@ protected:
        \brief Reset cancel flag of t if this was not canceled.
     */
     void parent_reset_cancel(tactic & t) {
-        #pragma omp critical (tactic_cancel)
-        {
-            if (!m_cancel) {
-                t.set_cancel(false);
-            }
+        if (!m_cancel) {
+            t.reset_cancel();
         }
     }
 
@@ -393,11 +390,8 @@ protected:
        \brief Reset cancel flag of st if this was not canceled.
     */
     void parent_reset_cancel(tactic & t) {
-        #pragma omp critical (tactic_cancel)
-        {
-            if (!m_cancel) {
-                t.set_cancel(false);
-            }
+        if (!m_cancel) {
+            t.reset_cancel();
         }
     }
 
@@ -988,7 +982,7 @@ protected:
     virtual void set_cancel(bool f) { 
         m_cancel = f;
         if (m_t) 
-            m_t->set_cancel(f); 
+            m_t->set_cancel(f);
     }
 
     template<typename T>
diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index 14a42ec51..2f0262fc8 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -144,17 +144,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index 393a40603..cea8f2cfc 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -151,17 +151,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
index 0705c627c..efecb38ba 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
@@ -119,17 +119,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {