diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index e1d61d82c4..2f6d11601e 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -824,15 +824,16 @@ bool cmd_context::set_logic(symbol const & s) { TRACE("cmd_context", tout << s << "\n";); if (has_logic()) throw cmd_exception("the logic has already been set"); - if (has_manager() && m_main_ctx) + if (has_assertions() && m_main_ctx) throw cmd_exception("logic must be set before initialization"); - if (!smt_logics::supported_logic(s)) { + if (!smt_logics::supported_logic(s)) return false; - } + m_logic = s; - if (smt_logics::logic_has_reals_only(s)) { + if (m_solver) + mk_solver(); + if (smt_logics::logic_has_reals_only(s)) m_numeral_as_real = true; - } return true; }