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

Thanks to David Cok for reporting these issues.

1 files changed, 5 insertions, 1 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,