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, 8 deletions

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;