diff options
Diffstat (limited to 'test/regress/README.md')
| -rw-r--r-- | test/regress/README.md | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/test/regress/README.md b/test/regress/README.md index 2c347bc48..34cf7efde 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -16,7 +16,16 @@ For example: TEST_REGEX=quantifiers make regress0 ``` -Runs regression tests from level 0 that have "quantifiers" in their name. +This runs regression tests from level 0 that have "quantifiers" in their name. + +By default, each invocation of CVC4 is done with a 10 minute timeout. To use a +different timeout, set the `TEST_TIMEOUT` environment variable: + +``` +TEST_TIMEOUT=0.5s make regress0 +``` + +This runs regression tests from level 0 with a 0,5 second timeout. ## Adding New Regressions |