Better error on invalid logic strings.

Thanks to David Cok for reporting this issue.

4 files changed, 17 insertions, 11 deletions

diff --git a/library_versions b/library_versions
index eac360c34..7174f7b0b 100644
--- a/library_versions
+++ b/library_versions
@@ -53,3 +53,4 @@
 1\.2 libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0
 1\.2\.1-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0
 1\.3-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0
+# note: SmtEngine::setLogicString() exceptions have changed, bump library version on next release?
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 908ad05e2..ab4b13d4c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -792,21 +792,21 @@ SmtEngine::~SmtEngine() throw() {
 
 void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
   SmtScope smts(this);
-
   d_logic = logic;
   setLogicInternal();
 }
 
-void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
+void SmtEngine::setLogic(const std::string& s) throw(ModalException, LogicException) {
   SmtScope smts(this);
-
-  setLogic(LogicInfo(s));
+  try {
+    setLogic(LogicInfo(s));
+  } catch(IllegalArgumentException& e) {
+    throw LogicException(e.what());
+  }
 }
 
-void SmtEngine::setLogic(const char* logic) throw(ModalException){
-  SmtScope smts(this);
-
-  setLogic(LogicInfo(string(logic)));
+void SmtEngine::setLogic(const char* logic) throw(ModalException, LogicException) {
+  setLogic(string(logic));
 }
 
 LogicInfo SmtEngine::getLogicInfo() const {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a22e34c21..8266bb1ed 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -350,12 +350,12 @@ public:
   /**
    * Set the logic of the script.
    */
-  void setLogic(const std::string& logic) throw(ModalException);
+  void setLogic(const std::string& logic) throw(ModalException, LogicException);
 
   /**
    * Set the logic of the script.
    */
-  void setLogic(const char* logic) throw(ModalException);
+  void setLogic(const char* logic) throw(ModalException, LogicException);
 
   /**
    * Set the logic of the script.
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index dc9de8662..cbd0b510e 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -241,7 +241,12 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc
   }
   if(*p != '\0') {
     stringstream err;
-    err << "LogicInfo::setLogicString(): junk (\"" << p << "\") at end of logic string: " << logicString;
+    err << "LogicInfo::setLogicString(): ";
+    if(p == logicString) {
+      err << "cannot parse logic string: " << logicString;
+    } else {
+      err << "junk (\"" << p << "\") at end of logic string: " << logicString;
+    }
     IllegalArgument(logicString, err.str().c_str());
   }