From dec87fe4d970d0b59480fe85773bbaf177566137 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Jul 2022 16:19:12 -0700 Subject: [PATCH] fix issue with set-logic for eval_smtlib2_string --- src/cmd_context/cmd_context.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) 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; }