From: Tim King <taking@cs.nyu.edu>
Date: Wed, 6 Jan 2016 08:10:36 +0000 (-0800)
Subject: Improving the documentation of the CVC command CONTINUE.
X-Git-Tag: cvc5-1.0.0~6117
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0ef178e46acefc03373add0ed9a99c657bd4f72;p=cvc5.git

Improving the documentation of the CVC command CONTINUE.
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index efa51963a..5c477f2e2 100644
--- 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 edc868a79..3550174d8 100644
--- 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;
+
+