summaryrefslogtreecommitdiff
path: root/test/regress/regress0/push-pop/test.01.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/push-pop/test.01.cvc')
-rw-r--r--test/regress/regress0/push-pop/test.01.cvc7
1 files changed, 6 insertions, 1 deletions
diff --git a/test/regress/regress0/push-pop/test.01.cvc b/test/regress/regress0/push-pop/test.01.cvc
index 6110c6576..90be7d784 100644
--- a/test/regress/regress0/push-pop/test.01.cvc
+++ b/test/regress/regress0/push-pop/test.01.cvc
@@ -1,13 +1,18 @@
x, y: BOOLEAN;
ASSERT (x OR y);
+% EXPECT: sat
CHECKSAT;
PUSH;
ASSERT (NOT x);
+% EXPECT: sat
CHECKSAT;
POP;
PUSH;
ASSERT (NOT y);
+% EXPECT: sat
CHECKSAT;
POP;
-CHECKSAT; \ No newline at end of file
+% EXPECT: sat
+CHECKSAT;
+% EXIT: 10
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback