Minor cleanup in SolverEngine::setInfo() (#7566)
authorGereon Kremer <nafur42@gmail.com>
Thu, 4 Nov 2021 15:31:31 +0000 (08:31 -0700)
committerGitHub <noreply@github.com>
Thu, 4 Nov 2021 15:31:31 +0000 (15:31 +0000)
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.

src/smt/solver_engine.cpp

index fc6ec391563aa632975f7bb9d14c3afe0fd64c80..c7147a67635162500c21866f58481039e76b8c0e 100644 (file)
@@ -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")