diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/push-pop/units.cvc | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test/regress/regress0/push-pop/units.cvc b/test/regress/regress0/push-pop/units.cvc new file mode 100644 index 000000000..9bdfdaadb --- /dev/null +++ b/test/regress/regress0/push-pop/units.cvc @@ -0,0 +1,20 @@ +% COMMAND-LINE: --incremental +x, y: BOOLEAN; +ASSERT x OR y; +% EXPECT: sat +CHECKSAT; +PUSH; + ASSERT NOT x; +% EXPECT: sat + CHECKSAT; + PUSH; + ASSERT NOT y; +% EXPECT: unsat + CHECKSAT; + POP; +% EXPECT: sat + CHECKSAT; +POP; +% EXPECT: sat +CHECKSAT; +% EXIT: 10 |