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());