From df5f7fe03fda041429548bcb39abb8916ca2e291 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 9 Nov 2010 21:57:06 +0000
Subject: Lemmas on demand work, push-pop, some cleanup.

---
 test/regress/regress0/push-pop/test.01.cvc | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test/regress/regress0/push-pop/test.01.cvc

(limited to 'test/regress/regress0/push-pop/test.01.cvc')

diff --git a/test/regress/regress0/push-pop/test.01.cvc b/test/regress/regress0/push-pop/test.01.cvc
new file mode 100644
index 000000000..6110c6576
--- /dev/null
+++ b/test/regress/regress0/push-pop/test.01.cvc
@@ -0,0 +1,13 @@
+x, y: BOOLEAN;
+
+ASSERT (x OR y);
+CHECKSAT;
+PUSH;
+ASSERT (NOT x);
+CHECKSAT;
+POP;
+PUSH;
+ASSERT (NOT y);
+CHECKSAT;
+POP;
+CHECKSAT;
\ No newline at end of file
-- 
cgit v1.2.3