diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-16 21:08:38 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-16 21:08:38 -0700 |
| commit | 8b9baa66ad6ffc9e323b83bc967992439a7d9bfa (patch) | |
| tree | bdb58c5a3249dc5f573284c306d529e4e3bd8067 /test/regress/README.md | |
| parent | 8a079f9b982a502995da8e535a4b4487489af0d2 (diff) | |
Add timeout (option) to regression script (#1786)
This commit adds the option to run regressions with a timeout using the
`TEST_TIMEOUT` environment variable. The default timeout is set to 10
minutes. This should make it less likely that our nightly builds hang
and makes it easier to sort out slow tests.
Default timeout tested with regression level 2 on a debug build with
proofs.
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 |