From 1b0ac4940b9be79435153b94d6ea29f27fea62ef Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Dec 2021 11:51:00 -0800
Subject: [PATCH] prevent stale user-propagators from being used on the same
 tactic after it was applied.

---
 src/smt/tactic/smt_tactic_core.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index a9fd2fc729e..d6b2d411461 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -140,6 +140,7 @@ class smt_tactic : public tactic {
         ~scoped_init_ctx() {
             smt::kernel * d = m_owner.m_ctx;
             m_owner.m_ctx = nullptr;
+            m_owner.m_user_ctx = nullptr;
 
             if (d)
                 dealloc(d);