diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-11-16 19:18:19 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-11-16 19:18:19 +0000 |
| commit | e66924cb0f425ca70969058532340e68c9c17a54 (patch) | |
| tree | 6dfdb2d02621c45a17b9ca3202cc3db7c30d7da5 /test/regress/regress0/push-pop | |
| parent | d5d504da7c73538642b9be86c73f8407e08ab57a (diff) | |
SmtEngine now fails with a ModalException if --incremental is not enabled
but a push/pop or multiple query is attempted (previously it could give
incorrect answers)
Also, fix some multi-query and push-pop tests that had wrong answers, and
support a new "% COMMAND-LINE: " gesture in regression tests so that a
test can pass additional, specific command line flags it wants to run
with (here, --incremental).
Also fix mkbuilddir script for when it's called from contrib/switch-config.
Diffstat (limited to 'test/regress/regress0/push-pop')
| -rw-r--r-- | test/regress/regress0/push-pop/test.00.cvc | 5 | ||||
| -rw-r--r-- | test/regress/regress0/push-pop/test.01.cvc | 2 |
2 files changed, 5 insertions, 2 deletions
diff --git a/test/regress/regress0/push-pop/test.00.cvc b/test/regress/regress0/push-pop/test.00.cvc index 38d720227..f56abb386 100644 --- a/test/regress/regress0/push-pop/test.00.cvc +++ b/test/regress/regress0/push-pop/test.00.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: --incremental x: BOOLEAN; PUSH; @@ -6,6 +7,6 @@ ASSERT x; CHECKSAT; POP; ASSERT (NOT x); -% EXPECT: unsat +% EXPECT: sat CHECKSAT; -% EXIT: 20 +% EXIT: 10 diff --git a/test/regress/regress0/push-pop/test.01.cvc b/test/regress/regress0/push-pop/test.01.cvc index 90be7d784..5d492db32 100644 --- a/test/regress/regress0/push-pop/test.01.cvc +++ b/test/regress/regress0/push-pop/test.01.cvc @@ -1,3 +1,5 @@ +% COMMAND-LINE: --incremental + x, y: BOOLEAN; ASSERT (x OR y); |