Improving the documentation of the CVC command CONTINUE.

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index efa51963ad5de845afaa56cc6c6f6a57b570bdce..5c477f2e24172ed4739e4bc56a23831fcbb24445 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -79,6 +79,7 @@ tokens {
   COUNTEREXAMPLE_TOK = 'COUNTEREXAMPLE';
   COUNTERMODEL_TOK = 'COUNTERMODEL';
   ARITH_VAR_ORDER_TOK = 'ARITH_VAR_ORDER';
+  CONTINUE_TOK = 'CONTINUE';
 
   /* operators */
 
@@ -831,6 +832,9 @@ mainCommand[CVC4::Command*& cmd]
   | ARITH_VAR_ORDER_TOK LPAREN formula[f] ( COMMA formula[f] )* RPAREN
     { UNSUPPORTED("ARITH_VAR_ORDER command"); }
 
+  | CONTINUE_TOK
+    { UNSUPPORTED("CONTINUE command"); }
+
   | toplevelDeclaration[cmd]
   ;
 

diff --git a/test/regress/regress0/push-pop/units.cvc b/test/regress/regress0/push-pop/units.cvc
index edc868a792df76dff359cb72cdce0c040a7acaa1..3550174d838987daf2499e048a6dccbdd7f7ef02 100644 (file)
--- a/test/regress/regress0/push-pop/units.cvc
+++ b/test/regress/regress0/push-pop/units.cvc
@@ -17,3 +17,13 @@ PUSH;
 POP;
 % EXPECT: sat
 CHECKSAT;
+PUSH 2;
+ASSERT x;
+ASSERT NOT x;
+% EXPECT: unsat
+CHECKSAT;
+POP 2;
+% EXPECT: sat
+CHECKSAT;
+
+