cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2020-07-01	Add testing infrastructure for LFSC signatures (#4678)	Andres Noetzli
	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
2017-01-04	Marking the proof signature files as non-executable.	Tim King

2016-01-26	Merged bit-vector and uf proof branch.	Liana Hadarean

2014-03-19	Fix a memory leak in LFSC proof checker. Largest QF_UF proof from Morgan ↵	Andrew Reynolds
	(problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory. Add example test proof.