From 9790a8aa439ca9b94785f471143ce0cdda21fd95 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Aug 2021 09:42:40 -0700
Subject: [PATCH] #5507

can't use auto-config if there are no assertions. Auto-config only works properly for one-shot mode since theories aren't loaded on demand in this solver.
---
 src/smt/smt_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index b54196ac42b..71aeebd6a61 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2880,7 +2880,7 @@ namespace smt {
         solver::push_eh_t&       push_eh,
         solver::pop_eh_t&        pop_eh,
         solver::fresh_eh_t&      fresh_eh) {
-        setup_context(m_fparams.m_auto_config);
+        setup_context(false);
         m_user_propagator = alloc(user_propagator, *this);
         m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
         for (unsigned i = m_scopes.size(); i-- > 0; )