Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places

Thanks to David Cok for reporting these issues.

2 files changed, 12 insertions, 2 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 3376e9d0b..5c9f8af21 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -313,7 +313,11 @@ restart:
     line += "\n";
     goto restart;
   } catch(ParserException& pe) {
-    d_out << pe << endl;
+    if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2) {
+      d_out << "(error \"" << pe << "\")" << endl;
+    } else {
+      d_out << pe << endl;
+    }
     // We can't really clear out the sequence and abort the current line,
     // because the parse error might be for the second command on the
     // line.  The first ones haven't yet been executed by the SmtEngine,
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 7b61b48aa..a4c4b9c0a 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -37,10 +37,12 @@
 #include "util/output.h"
 #include "util/result.h"
 #include "util/statistics.h"
+#include "util/language.h"
 
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::main;
+using namespace CVC4::language;
 
 /**
  * CVC4's main() routine is just an exception-safe wrapper around CVC4.
@@ -64,7 +66,11 @@ int main(int argc, char* argv[]) {
 #ifdef CVC4_COMPETITION_MODE
     *opts[options::out] << "unknown" << endl;
 #endif
-    *opts[options::err] << "CVC4 Error:" << endl << e << endl;
+    if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2) {
+      *opts[options::err] << "(error \"" << e << "\")" << endl;
+    } else {
+      *opts[options::err] << "CVC4 Error:" << endl << e << endl;
+    }
     if(opts[options::statistics] && pExecutor != NULL) {
       pTotalTime->stop();
       pExecutor->flushStatistics(*opts[options::err]);