From 9ce4c3153d42bc079470b7bd73bf131499b3fcbe Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 1 Jul 2020 08:44:21 -0700 Subject: Add testing infrastructure for LFSC signatures (#4678) 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 --- proofs/signatures/lrat.plf | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/signatures/lrat.plf') diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf index d16791624..b5d46be43 100644 --- a/proofs/signatures/lrat.plf +++ b/proofs/signatures/lrat.plf @@ -2,7 +2,7 @@ ; LRAT format detailed in "Efficient Certified RAT Verification" ; Link: https://www.cs.utexas.edu/~marijn/publications/lrat.pdf ; Author: aozdemir -; Depends On: sat.plf, smt.plf +; Deps: sat.plf smt.plf ; A general note about the design of the side conditions: -- cgit v1.2.3