3 files changed, 14 insertions, 15 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9ceed82f7..de6f614e1 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -158,32 +158,32 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
   }
   const char* filename = filenameStr.c_str();
 
-  if (opts->base.inputLanguage == language::input::LANG_AUTO)
+  if (opts->base.inputLanguage == Language::LANG_AUTO)
   {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
-      opts->base.inputLanguage = language::input::LANG_CVC;
+      opts->base.inputLanguage = Language::LANG_CVC;
     } else {
       size_t len = filenameStr.size();
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        opts->base.inputLanguage = language::input::LANG_SMTLIB_V2_6;
+        opts->base.inputLanguage = Language::LANG_SMTLIB_V2_6;
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
-        opts->base.inputLanguage = language::input::LANG_TPTP;
+        opts->base.inputLanguage = Language::LANG_TPTP;
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        opts->base.inputLanguage = language::input::LANG_CVC;
+        opts->base.inputLanguage = Language::LANG_CVC;
       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
         // version 2 sygus is the default
-        opts->base.inputLanguage = language::input::LANG_SYGUS_V2;
+        opts->base.inputLanguage = Language::LANG_SYGUS_V2;
       }
     }
   }
 
-  if (opts->base.outputLanguage == language::output::LANG_AUTO)
+  if (opts->base.outputLanguage == Language::LANG_AUTO)
   {
-    opts->base.outputLanguage = language::toOutputLanguage(opts->base.inputLanguage);
+    opts->base.outputLanguage = opts->base.inputLanguage;
   }
   pExecutor->storeOptionsAsOriginal();
 
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 7a1ee89ab..14a507aee 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -116,23 +116,22 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
 #endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
     ::using_history();
 
-    OutputLanguage lang =
-        toOutputLanguage(d_options.base.inputLanguage);
+    Language lang = d_options.base.inputLanguage;
     switch(lang) {
-      case output::LANG_CVC:
+      case Language::LANG_CVC:
         d_historyFilename = string(getenv("HOME")) + "/.cvc5_history";
         commandsBegin = cvc_commands;
         commandsEnd =
             cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
         break;
-      case output::LANG_TPTP:
+      case Language::LANG_TPTP:
         d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp";
         commandsBegin = tptp_commands;
         commandsEnd =
             tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
         break;
       default:
-        if (language::isOutputLang_smt2(lang))
+        if (language::isLangSmt2(lang))
         {
           d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2";
           commandsBegin = smt2_commands;
@@ -365,7 +364,7 @@ restart:
   }
   catch (ParserException& pe)
   {
-    if (language::isOutputLang_smt2(d_options.base.outputLanguage))
+    if (language::isLangSmt2(d_options.base.outputLanguage))
     {
       d_out << "(error \"" << pe << "\")" << endl;
     }
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 6f109255f..5fedc53da 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -79,7 +79,7 @@ int main(int argc, char* argv[])
 #ifdef CVC5_COMPETITION_MODE
     *solver->getOptions().base.out << "unknown" << endl;
 #endif
-    if (language::isOutputLang_smt2(solver->getOptions().base.outputLanguage))
+    if (language::isLangSmt2(solver->getOptions().base.outputLanguage))
     {
       *solver->getOptions().base.out << "(error \"" << e << "\")" << endl;
     }