clear tactic user propagate state on solver destructor

Z3Prover · Dec 7, 2021 · 658a334 · 658a334
1 parent fdc253a
commit 658a334
Show file tree

Hide file tree

Showing 4 changed files with 23 additions and 5 deletions.
diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
@@ -413,16 +413,21 @@ class smt_tactic : public tactic {
         }    
     }
 
-    void user_propagate_init(
-        void* ctx,
-        user_propagator::push_eh_t& push_eh,
-        user_propagator::pop_eh_t& pop_eh,
-        user_propagator::fresh_eh_t& fresh_eh) override {
+    void user_propagate_clear() override {
+        m_user_ctx = nullptr;
         m_vars.reset();
         m_fixed_eh = nullptr;
         m_final_eh = nullptr;
         m_eq_eh = nullptr;
         m_diseq_eh = nullptr;
+    }
+
+    void user_propagate_init(
+        void* ctx,
+        user_propagator::push_eh_t& push_eh,
+        user_propagator::pop_eh_t& pop_eh,
+        user_propagator::fresh_eh_t& fresh_eh) override {
+        user_propagate_clear();
         m_user_ctx = ctx;
         m_push_eh = push_eh;
         m_pop_eh = pop_eh;

diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
@@ -112,6 +112,11 @@ class tactic2solver : public solver_na2as {
         return m_tactic->user_propagate_register(e);
     }
 
+    void user_propagate_clear() override {
+        if (m_tactic)
+            m_tactic->user_propagate_clear();
+    }
+
 
     expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override {
         set_reason_unknown("cubing is not supported on tactics");
@@ -148,6 +153,7 @@ tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p,
 }
 
 tactic2solver::~tactic2solver() {
+    user_propagate_clear();
 }
 
 void tactic2solver::updt_params(params_ref const & p) {

diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
@@ -192,6 +192,10 @@ class and_then_tactical : public binary_tactical {
         return m_t2->user_propagate_register(e);
     }
 
+    void user_propagate_clear() override {
+        m_t2->user_propagate_clear();
+    }
+
 };
 
 tactic * and_then(tactic * t1, tactic * t2) {

diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h
@@ -56,6 +56,9 @@ namespace user_propagator {
         virtual unsigned user_propagate_register(expr* e) { 
             throw default_exception("user-propagators are only supported on the SMT solver");
         }
+
+        virtual void user_propagate_clear() {
+        }
 
     };