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/regress1/quantifiers | |
| 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/regress1/quantifiers')
| -rw-r--r-- | test/regress/regress1/quantifiers/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/set3.smt2 | 1 |
2 files changed, 3 insertions, 1 deletions
diff --git a/test/regress/regress1/quantifiers/Makefile.am b/test/regress/regress1/quantifiers/Makefile.am index 159f2e088..af277af90 100644 --- a/test/regress/regress1/quantifiers/Makefile.am +++ b/test/regress/regress1/quantifiers/Makefile.am @@ -80,7 +80,8 @@ TESTS = \ RNDPRE_4_1-dd-nqe.smt2 \ set8.smt2 \ z3.620661-no-fv-trigger.smt2 \ - arith-rec-fun.smt2 + arith-rec-fun.smt2 \ + set3.smt2 # removed because they take more than 20s # javafe.ast.ArrayInit.35.smt2 diff --git a/test/regress/regress1/quantifiers/set3.smt2 b/test/regress/regress1/quantifiers/set3.smt2 index d3e51d996..bd208c6d3 100644 --- a/test/regress/regress1/quantifiers/set3.smt2 +++ b/test/regress/regress1/quantifiers/set3.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --full-saturate-quant (set-logic AUFLIA) (set-info :source | Assertion verification of simple set manipulation programs. |) (set-info :smt-lib-version 2.0) |