summaryrefslogtreecommitdiff
path: root/proofs/signatures/sat.plf
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-04-05 21:45:17 -0700
committerGitHub <noreply@github.com>2018-04-05 21:45:17 -0700
commitefc6163629c6c5de446eccfe81777c93829995d5 (patch)
tree8681a332d409e94fc4ab7259513bc7935e5568b5 /proofs/signatures/sat.plf
parentcf73e3ceb3f93fef830349bd44afec99404b5038 (diff)
Python regression script (#1662)
Until now, we have been using a bash script for the running the regressions. That script had several issues, e.g. it was creating many temprorary files and it was calling itself recursively, making it difficult to maintain. This commit replaces the script with a Python script. The Python script uses the TAP protocol, which allows us to display the results of multiple tests per file (e.g. with --check-models and without) separately and with more details. It also outputs whenever it starts running a test, which allows finding "stuck" regression tests on Travis. As recommended in the automake documentation [0], the commit copies the TAP driver to enable TAP support for the test driver. Note: the commit also changes some of the regressions slightly because we were using "%" for the test directives in SMT files which does not correspond to the comment character ";". Using the comment character simplifies the handling and makes it easier for users to reproduce a failure (they can simply run CVC4 on the regression file). [0] https://www.gnu.org/software/automake/manual/html_node/Use-TAP-with-the-Automake-test-harness.html
Diffstat (limited to 'proofs/signatures/sat.plf')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback