summaryrefslogtreecommitdiff
path: root/test/regress/regress0/fmf/Makefile.am
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-03-21 09:41:50 -0700
committerGitHub <noreply@github.com>2018-03-21 09:41:50 -0700
commitbe2702490d684c100ba6abe76ee156078a9aa621 (patch)
tree8b22bc7e38aad39da092b409dded4d2ce84b4047 /test/regress/regress0/fmf/Makefile.am
parent8f0aae827e16f4dfcebb8dad2cc528649d40b16a (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/fmf/Makefile.am')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback