From 68b072e7f147738c3ab3431ae1398cc6dba3773b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Dec 2021 09:22:25 -0800
Subject: [PATCH] only use setup_and_check if there is no user propagator set.

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

diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index b9e8e63e0..b6c8b5e55 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -200,7 +200,7 @@ public:
 
             lbool r;
             try {
-                if (assumptions.empty())
+                if (assumptions.empty() && !m_user_ctx)
                     r = m_ctx->setup_and_check();
                 else
                     r = m_ctx->check(assumptions.size(), assumptions.data());