Add support for check-sat with argument.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 23f0fb9fabbdfe374556173b57f70b648147ea27..a6a2aa58c8fff2f3bf2e6c84b9620ea5f2b4c264 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -344,7 +344,13 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new AssertCommand(expr); }
   | /* checksat */
     CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { cmd = new CheckSatCommand(MK_CONST(bool(true))); }
+    ( term[expr, expr2]
+      { if(PARSER_STATE->strictModeEnabled()) {
+          PARSER_STATE->parseError("Extended commands (such as check-sat with an argument) are not permitted while operating in strict compliance mode.");
+        }
+      }
+    | { expr = MK_CONST(bool(true)); } )
+    { cmd = new CheckSatCommand(expr); }
   | /* get-assertions */
     GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd = new GetAssertionsCommand(); }

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 1dbaf7cdf8be2eef223d1b424b030b05cb509aca..8ff62c25a47e61dcf2c5166aae9a404df940f881 100644 (file)
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -395,7 +395,7 @@ public:
 #ifndef CVC4_COMPETITION_MODE
     tryBadInput("(assert)"); // no args
     tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
-    tryBadInput("(set-logic QF_UF) (check-sat true)"); // shouldn't have an arg
+    tryBadInput("(set-logic QF_UF) (check-sat true)", true); // check-sat shouldn't have an arg
     tryBadInput("(declare-sort a)"); // no arg
     tryBadInput("(declare-sort a 0) (declare-sort a 0)"); // double decl
     tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); // should be "p () Bool"