1 files changed, 27 insertions, 19 deletions

diff --git a/src/options/language.cpp b/src/options/language.cpp
index 8261271fb..13384164a 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -73,7 +73,7 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   switch(language) {
   case output::LANG_SMTLIB_V2_6:
   case output::LANG_TPTP:
-  case output::LANG_CVC4:
+  case output::LANG_CVC:
   case output::LANG_SYGUS_V2:
     // these entries directly correspond (by design)
     return InputLanguage(int(language));
@@ -91,7 +91,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   switch(language) {
   case input::LANG_SMTLIB_V2_6:
   case input::LANG_TPTP:
-  case input::LANG_CVC4:
+  case input::LANG_CVC:
   case input::LANG_SYGUS_V2:
     // these entries directly correspond (by design)
     return OutputLanguage(int(language));
@@ -104,7 +104,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
     // it's better to output SOMETHING related to the original
     // exception rather than mask it with another exception.  Also,
     // the input language isn't always defined---e.g. during the
-    // initial phase of the main CVC4 driver while it determines which
+    // initial phase of the main cvc5 driver while it determines which
     // language is appropriate, and during unit tests.  Also, when
     // users are writing their own code against the library.
     return output::LANG_AST;
@@ -112,11 +112,13 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
 }/* toOutputLanguage() */
 
 OutputLanguage toOutputLanguage(std::string language) {
-  if(language == "cvc4" || language == "pl" ||
-     language == "presentation" || language == "native" ||
-     language == "LANG_CVC4") {
-    return output::LANG_CVC4;
-  } else if(language == "cvc3" || language == "LANG_CVC3") {
+  if (language == "cvc4" || language == "pl" || language == "presentation"
+      || language == "native" || language == "LANG_CVC")
+  {
+    return output::LANG_CVC;
+  }
+  else if (language == "cvc3" || language == "LANG_CVC3")
+  {
     return output::LANG_CVC3;
   }
   else if (language == "smtlib" || language == "smt" || language == "smtlib2"
@@ -146,19 +148,25 @@ OutputLanguage toOutputLanguage(std::string language) {
 }/* toOutputLanguage() */
 
 InputLanguage toInputLanguage(std::string language) {
-  if(language == "cvc4" || language == "pl" ||
-     language == "presentation" || language == "native" ||
-     language == "LANG_CVC4") {
-    return input::LANG_CVC4;
-  } else if(language == "smtlib" || language == "smt" ||
-            language == "smtlib2" || language == "smt2" ||
-            language == "smtlib2.6" || language == "smt2.6" ||
-            language == "LANG_SMTLIB_V2_6" || language == "LANG_SMTLIB_V2") {
+  if (language == "cvc4" || language == "pl" || language == "presentation"
+      || language == "native" || language == "LANG_CVC")
+  {
+    return input::LANG_CVC;
+  }
+  else if (language == "smtlib" || language == "smt" || language == "smtlib2"
+           || language == "smt2" || language == "smtlib2.6"
+           || language == "smt2.6" || language == "LANG_SMTLIB_V2_6"
+           || language == "LANG_SMTLIB_V2")
+  {
     return input::LANG_SMTLIB_V2_6;
-  } else if(language == "tptp" || language == "LANG_TPTP") {
+  }
+  else if (language == "tptp" || language == "LANG_TPTP")
+  {
     return input::LANG_TPTP;
-  } else if(language == "sygus" || language == "sygus2" ||
-          language == "LANG_SYGUS" || language == "LANG_SYGUS_V2") {
+  }
+  else if (language == "sygus" || language == "sygus2"
+           || language == "LANG_SYGUS" || language == "LANG_SYGUS_V2")
+  {
     return input::LANG_SYGUS_V2;
   }
   else if (language == "auto" || language == "LANG_AUTO")