2 files changed, 7 insertions, 0 deletions
diff --git a/src/util/language.cpp b/src/util/language.cpp
index 8a1ab26af..1a184e648 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -68,6 +68,8 @@ OutputLanguage toOutputLanguage(std::string language) {
      language == "presentation" || language == "native" ||
      language == "LANG_CVC4") {
     return output::LANG_CVC4;
+  } else if(language == "cvc3" || language == "LANG_CVC3") {
+    return output::LANG_CVC3;
   } else if(language == "smtlib1" || language == "smt1" ||
             language == "LANG_SMTLIB_V1") {
     return output::LANG_SMTLIB_V1;
diff --git a/src/util/language.h b/src/util/language.h
index c79c4d9aa..0d1c5486a 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -121,6 +121,8 @@ enum CVC4_PUBLIC Language {
 
   /** The AST output language */
   LANG_AST = 10,
+  /** The CVC3-compatibility output language */
+  LANG_CVC3,
 
   /** LANG_MAX is > any valid OutputLanguage id */
   LANG_MAX
@@ -147,6 +149,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_AST:
     out << "LANG_AST";
     break;
+  case LANG_CVC3:
+    out << "LANG_CVC3";
+    break;
   default:
     out << "undefined_output_language";
   }