From: E Polgreen <epolgreen@gmail.com>
Date: Fri, 14 Aug 2020 17:19:09 +0000 (-0700)
Subject: correctly parse sygus lang option (#4884)
X-Git-Tag: cvc5-1.0.0~3002
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ee055dddf887ed001fee1834ba845fb81e20e27e;p=cvc5.git

correctly parse sygus lang option (#4884)

--lang sygus is a synonym for --lang sygus2
also fixes typo in error message for language options parsing

Signed-off-by: polgreen <epolgreen@gmail.com>
---

diff --git a/src/options/language.cpp b/src/options/language.cpp
index b00d5c102..a5b5c888b 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -181,9 +181,8 @@ InputLanguage toInputLanguage(std::string language) {
     return input::LANG_SMTLIB_V2_6;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
-  }
-  else if (language == "sygus2" || 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")
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index b752bfdda..1b18dd7f4 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -538,7 +538,7 @@ InputLanguage OptionsHandler::stringToInputLanguage(std::string option,
   try {
     return language::toInputLanguage(optarg);
   } catch(OptionException& oe) {
-    throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --language help");
+    throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --lang help");
   }
 
   Unreachable();