diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-08 23:16:13 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-08 23:16:13 -0700 |
| commit | 106e764a04e4099cc36d13de9cec47cbf717b6cc (patch) | |
| tree | 9535bb7750fe7bc0072ab7c78f1e667d0d054f6d /test/regress/README.md | |
| parent | 6104c154e07b6d343b4d08c7bd185f6d74c89da8 (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.
Diffstat (limited to 'test/regress/README.md')
| -rw-r--r-- | test/regress/README.md | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/test/regress/README.md b/test/regress/README.md index d0c9b2b7a..772332c3e 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -116,10 +116,11 @@ a given benchmark when a feature is supported. For example: ; REQUIRES: symfpu ``` -This benchmark is only run when symfpu has been configured. -Multiple `REQUIRES` directives are supported. For a list of -features that can be listed as a requirement, refer to CVC4's -`--show-config` output. +This benchmark is only run when symfpu has been configured. Multiple +`REQUIRES` directives are supported. For a list of features that can be listed +as a requirement, refer to CVC4's `--show-config` output. Features can also be +excluded by adding the `no-` prefix, e.g. `no-symfpu` means that the test is +not valid for builds that include symfpu support. Sometimes it is useful to keep the directives separate. You can separate the benchmark from the output expectations by putting the benchmark in `<benchmark |