projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6104c15) | patch
Add flag to skip regression if feature enabled (#2062)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 9 Jun 2018 06:16:13 +0000 (23:16 -0700)
committerGitHub <noreply@github.com>
Sat, 9 Jun 2018 06:16:13 +0000 (23:16 -0700)
commit106e764a04e4099cc36d13de9cec47cbf717b6cc
tree9535bb7750fe7bc0072ab7c78f1e667d0d054f6dtree
parent6104c154e07b6d343b4d08c7bd185f6d74c89da8commit | diff
Add flag to skip regression if feature enabled (#2062)

This commit adds the option of skipping regressions when a specified
feature is enabled. It also changes some of the regression tests to be
skipped when it is a competition build because regressions fail
otherwise. In the tests changed in this commit, we do not care about
reproducing error messages in a competition build, so we can skip them.
test/regress/README.md diff | blob | history
test/regress/regress1/arrayinuf_error.smt2 diff | blob | history
test/regress/regress1/datatypes/error.cvc diff | blob | history
test/regress/regress1/errorcrash.smt2 diff | blob | history
test/regress/run_regression.py diff | blob | history