mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
fix issue with set-logic for eval_smtlib2_string
This commit is contained in:
parent
1378e713ba
commit
dec87fe4d9
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue