diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-03-21 09:41:50 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-21 09:41:50 -0700 |
| commit | be2702490d684c100ba6abe76ee156078a9aa621 (patch) | |
| tree | 8b22bc7e38aad39da092b409dded4d2ce84b4047 /test/regress/regress0/uf | |
| parent | 8f0aae827e16f4dfcebb8dad2cc528649d40b16a (diff) | |
Fix various regression tests (#1657)
While reorganizing the regression tests, I found three tests with a
wrong status, one that CVC4 reported unknown for and some regression
tests that had command line options set in the Makefile.am instead of
the tests themselves. This commit fixes the status of the three
regression tests (verified the status with Z3), adds command line
options to make the previously "unknown" test work, and moves the
command line options from the Makefile.am into the individual regression
tests. The latter also required some minor changes to the regression
script because it would not try to determine the expected output from
the (set-info :status ...) command if there was one directive (such as
EXPECT/COMMAND-LINE/etc.). This was an issue with the tests that now
have a COMMAND-LINE directive.
Diffstat (limited to 'test/regress/regress0/uf')
| -rw-r--r-- | test/regress/regress0/uf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/uf/pred.smt | 4 |
2 files changed, 4 insertions, 3 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index dd8621618..65f96f469 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -49,7 +49,8 @@ TESTS = \ cnf-ite.smt2 \ cnf-and-neg.smt2 \ cnf_abc.smt2 \ - bool-pred-nested.smt2 + bool-pred-nested.smt2 \ + pred.smt EXTRA_DIST = $(TESTS) \ mkpidgeon diff --git a/test/regress/regress0/uf/pred.smt b/test/regress/regress0/uf/pred.smt index e6f82727e..bdc49e7ce 100644 --- a/test/regress/regress0/uf/pred.smt +++ b/test/regress/regress0/uf/pred.smt @@ -1,5 +1,5 @@ -(benchmark euf_simp1.smt -:status sat +(benchmark pred.smt +:status unsat :logic QF_UF :category { crafted } |