summaryrefslogtreecommitdiff
path: root/src/util/language.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/language.h')
-rw-r--r--src/util/language.h5
1 files changed, 5 insertions, 0 deletions
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";
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback