diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2018-11-01 19:06:06 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-01 19:06:06 -0700 |
| commit | 050747cbceef232b11f1226081bc3dbc74c8ff77 (patch) | |
| tree | 857bce939a7f9df7e35e676982c5e1b2a149462c | |
| parent | f59097bfc7f89a30b2d857b0b43eb9130e85f45e (diff) | |
fixes to regression docs (#2679)
| -rw-r--r-- | INSTALL.md | 3 | ||||
| -rw-r--r-- | test/regress/README.md | 20 |
2 files changed, 7 insertions, 16 deletions
diff --git a/INSTALL.md b/INSTALL.md index 98cef2061..dc0de6cb4 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -151,7 +151,8 @@ provided with CVC4. ### CxxTest Unit Testing Framework (Unit Tests) [CxxTest](http://cxxtest.com) is required to optionally run CVC4's unit tests -(included with the distribution). See [Testing](testing) below for more details. +(included with the distribution). +See [Testing CVC4](#Testing-CVC4) below for more details. ## Building CVC4 diff --git a/test/regress/README.md b/test/regress/README.md index d43ebf337..28ccfb96b 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -3,20 +3,10 @@ ## Regression Levels and Running Regression Tests CVC4's regression tests are divided into 5 levels (level 0 to 4). Higher -regression levels are reserved for longer running regressions. To run -regressions up to a certain level use `make regressX` where `X` designates the -level. `make regress` by default runs levels 0 and 1. On Travis, we only run -regression level 0 to keep the time short. During our nightly builds, we run -regression level 2. +regression levels are reserved for longer running regressions. -To only run some benchmarks, you can use the `TEST_REGEX` environment variable. -For example: - -``` -TEST_REGEX=quantifiers make regress0 -``` - -This runs regression tests from level 0 that have "quantifiers" in their name. +For running regressions tests, +see the [INSTALL](https://github.com/CVC4/CVC4/blob/master/INSTALL.md#testing-cvc4) file. By default, each invocation of CVC4 is done with a 10 minute timeout. To use a different timeout, set the `TEST_TIMEOUT` environment variable: @@ -35,10 +25,10 @@ To add a new regression file, add the file to git, for example: git add regress/regress0/testMyFunctionality.cvc ``` -Also add it to [Makefile.tests](Makefile.tests) in this directory. +Also add it to [CMakeLists.txt](CMakeLists.txt) in this directory. A number of regressions exist under test/regress that are not listed in -[Makefile.tests](Makefile.tests). These are regressions that may someday be +[CMakeLists.txt](CMakeLists.txt). These are regressions that may someday be included in the standard suite of tests, but are not yet included (perhaps they test functionality not yet supported). |