From 658a334ecf5a06553ad16d2104440e892b31c31c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Dec 2021 03:11:54 -0800
Subject: [PATCH] clear tactic user propagate state on solver destructor

---
 src/smt/tactic/smt_tactic_core.cpp | 15 ++++++++++-----
 src/solver/tactic2solver.cpp       |  6 ++++++
 src/tactic/tactical.cpp            |  4 ++++
 src/tactic/user_propagator_base.h  |  3 +++
 4 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index d7ebce617a8..90c580b6718 100644
--- 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
index 0e949aa67ad..94f7fb336de 100644
--- 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
index 568bb792d4b..9b52546fc05 100644
--- 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
index ba3768921a3..d9645069d7f 100644
--- 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() {
+        }
        
     };