diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-20 20:23:09 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-20 20:23:09 -0700 |
| commit | 29b2e5a74eb007f04a18e01d7a9c21eff577c9b1 (patch) | |
| tree | b6ea5c072884fd78bd3a0dfec9b0b45ebf0d3b25 /test/regress/README.md | |
| parent | a82837a03cf3bd33f906901f45b2c6f36cf420de (diff) | |
Remove support for *.expect files in regressions (#2341)
Currently, we can optionally specify an *.expect file with the metadata
of a regression test. This commit removes that option because it was not
widely used, adds maintenance overhead and makes the transition to a new
build system more cumbersome. Regression files can still be fed to a
solver without removing the metadata first since they are in comments of
the corresponding input format (note that this was not always the case,
it changed in efc6163629c6c5de446eccfe81777c93829995d5).
Diffstat (limited to 'test/regress/README.md')
| -rw-r--r-- | test/regress/README.md | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/test/regress/README.md b/test/regress/README.md index e1ac79976..d43ebf337 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -121,9 +121,3 @@ This benchmark is only run when symfpu has been configured. Multiple 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 -file>.smt` and the directives in `<benchmark file>.smt.expect`, which is looked -for by the regression script. Note that `*.expect` files should be added to the -`EXTRA_DIST` variable in [Makefile.am](Makefile.am). |