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/Makefile.am | |
| 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/Makefile.am')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 9f4fdce89..73901c328 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -22,8 +22,8 @@ SMT_TESTS = \ let2.smt \ simple.smt \ simple2.smt \ - simple-lra.smt \ - simple-rdl.smt \ + simple-lra.smt \ + simple-rdl.smt \ simple-uf.smt # Regression tests for SMT2 inputs @@ -31,16 +31,16 @@ SMT2_TESTS = \ ite2.smt2 \ ite3.smt2 \ ite4.smt2 \ - simple-lra.smt2 \ - simple-rdl.smt2 \ - simple-rdl-definefun.smt2 \ + simple-lra.smt2 \ + simple-rdl.smt2 \ + simple-rdl-definefun.smt2 \ simple-uf.smt2 # Regression tests for PL inputs CVC_TESTS = \ boolean-prec.cvc \ hole6.cvc \ - ite.cvc \ + ite.cvc \ logops.01.cvc \ logops.02.cvc \ logops.03.cvc \ @@ -48,8 +48,8 @@ CVC_TESTS = \ logops.05.cvc \ simple.cvc \ smallcnf.cvc \ - test11.cvc \ test9.cvc \ + test11.cvc \ uf20-03.cvc \ wiki.01.cvc \ wiki.02.cvc \ @@ -83,11 +83,13 @@ BUG_TESTS = \ bug167.smt \ bug168.smt \ bug187.smt2 \ + bug216.smt2 \ bug220.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ + bug216.smt2.expect if CVC4_BUILD_PROFILE_COMPETITION else |