From d0ef178e46acefc03373add0ed9a99c657bd4f72 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 6 Jan 2016 00:10:36 -0800
Subject: [PATCH] Improving the documentation of the CVC command CONTINUE.

---
 src/parser/cvc/Cvc.g                     |  4 ++++
 test/regress/regress0/push-pop/units.cvc | 10 ++++++++++
 2 files changed, 14 insertions(+)

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;
+
+
-- 
2.30.2