mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Browse source 
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.
This commit is contained in:
Nikolaj Bjorner 2021-08-27 09:42:40 -07:00
parent 828fc72754
commit 9790a8aa43
1 changed files with 1 additions and 1 deletions

2
src/smt/smt_context.cpp
View file

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