fix issue with set-logic for eval_smtlib2_string

Z3Prover · Jul 13, 2022 · dec87fe · dec87fe
1 parent 1378e71
commit dec87fe
Showing 1 changed file with 6 additions and 5 deletions.
diff --git 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;
 }