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

Thanks to David Cok for reporting these issues.

4 files changed, 24 insertions, 10 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]);
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 1ca56dc06..d13fbf2d6 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -482,6 +482,7 @@ public:
     }
   }
 
+  inline size_t scopeLevel() const { return d_symtab->getLevel(); }
   inline void pushScope() { d_symtab->pushScope(); }
   inline void popScope() { d_symtab->popScope(); }
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6c98a5529..dbe1135b3 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -284,7 +284,7 @@ command returns [CVC4::Command* cmd = NULL]
     { $cmd = new GetValueCommand(terms); }
   | /* get-assignment */
     GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetAssignmentCommand; }
+    { cmd = new GetAssignmentCommand(); }
   | /* assertion */
     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     term[expr, expr2]
@@ -294,13 +294,13 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
   | /* get-assertions */
     GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetAssertionsCommand; }
+    { cmd = new GetAssertionsCommand(); }
   | /* get-proof */
     GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetProofCommand; }
+    { cmd = new GetProofCommand(); }
   | /* get-unsat-core */
     GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetUnsatCoreCommand; }
+    { cmd = new GetUnsatCoreCommand(); }
   | /* push */
     PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( k=INTEGER_LITERAL
@@ -324,12 +324,15 @@ command returns [CVC4::Command* cmd = NULL]
     | { if(PARSER_STATE->strictModeEnabled()) {
           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH.  Maybe you want (push 1)?");
         } else {
-          cmd = new PushCommand;
+          cmd = new PushCommand();
         }
       } )
   | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( k=INTEGER_LITERAL
       { unsigned n = AntlrInput::tokenToUnsigned(k);
+        if(n > PARSER_STATE->scopeLevel()) {
+          PARSER_STATE->parseError("Attempted to pop above the top stack frame.");
+        }
         if(n == 0) {
           cmd = new EmptyCommand();
         } else if(n == 1) {
@@ -349,11 +352,11 @@ command returns [CVC4::Command* cmd = NULL]
     | { if(PARSER_STATE->strictModeEnabled()) {
           PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP.  Maybe you want (pop 1)?");
         } else {
-          cmd = new PopCommand;
+          cmd = new PopCommand();
         }
       } )
   | EXIT_TOK
-    { cmd = new QuitCommand; }
+    { cmd = new QuitCommand(); }
 
     /* CVC4-extended SMT-LIB commands */
   | extendedCommand[cmd]
@@ -400,7 +403,7 @@ extendedCommand[CVC4::Command*& cmd]
       cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
   | /* get model */
     GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new GetModelCommand; }
+    { cmd = new GetModelCommand(); }
   | ECHO_TOK
     ( simpleSymbolicExpr[sexpr]
       { std::stringstream ss;