diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-30 20:36:48 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-30 20:36:48 -0700 |
| commit | c62980dab74b3db795961f90a4c49c463437a8eb (patch) | |
| tree | ee477518c506e16adb565009e94192e19162ce10 /test/regress/regress1/error.cvc | |
| parent | da165b9cbee366d4e77716617f2e2c794da9bd46 (diff) | |
Add testing infrastructure for LFSC signatures
This commit adds testing infrastructure for LFSC signatures that is
enabled when CVC4 is configured with LFSC. The testing infrastructure
adopts `run_test.py` from https://github.com/CVC4/LFSC with minor
modifications (mainly adding support for a list of include directories
that are searched to resolve *.plf dependencies). The commit uses the
existing examples and test files from `proofs/signatures` as the initial
set of tests.
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Diffstat (limited to 'test/regress/regress1/error.cvc')
0 files changed, 0 insertions, 0 deletions