From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 4 Nov 2021 15:31:31 +0000 (-0700)
Subject: Minor cleanup in SolverEngine::setInfo() (#7566)
X-Git-Tag: cvc5-1.0.0~895
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d8e3996674dd518555bfc432bc0414c66475e538;p=cvc5.git

Minor cleanup in SolverEngine::setInfo() (#7566)

This does a bit of cleanup by properly calling the option handler instead of trying to manually replicating it. This is way more robust in the face of modifications to the option handlers.
---

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index fc6ec3915..c7147a676 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -389,24 +389,18 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value)
   else if (key == "smt-lib-version"
            && !getOptions().base.inputLanguageWasSetByUser)
   {
-    Language ilang = Language::LANG_SMTLIB_V2_6;
-
     if (value != "2" && value != "2.6")
     {
       Warning() << "SMT-LIB version " << value
                 << " unsupported, defaulting to language (and semantics of) "
                    "SMT-LIB 2.6\n";
     }
-    getOptions().base.inputLanguage = ilang;
+    getOptions().base.inputLanguage = Language::LANG_SMTLIB_V2_6;
     // also update the output language
     if (!getOptions().base.outputLanguageWasSetByUser)
     {
-      Language olang = ilang;
-      if (d_env->getOptions().base.outputLanguage != olang)
-      {
-        getOptions().base.outputLanguage = olang;
-        *d_env->getOptions().base.out << language::SetLanguage(olang);
-      }
+      setOption("output-language", "smtlib2.6");
+      getOptions().base.outputLanguageWasSetByUser = false;
     }
   }
   else if (key == "status")