From 106e764a04e4099cc36d13de9cec47cbf717b6cc Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 8 Jun 2018 23:16:13 -0700 Subject: [PATCH] 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 | 9 +++++---- test/regress/regress1/arrayinuf_error.smt2 | 3 ++- test/regress/regress1/datatypes/error.cvc | 2 +- test/regress/regress1/errorcrash.smt2 | 3 ++- test/regress/run_regression.py | 8 +++++++- 5 files changed, 17 insertions(+), 8 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 `