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
2019-03-28	fix ex_bv.plf (#2905)	Haniel Barbosa

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

2015-04-23	A few more minor updates to match google repository with CVC4 repository	Clark Barrett
	(mostly whitespace differences).
2014-08-20	Update bv proof signature and example, after discussions with Liana.	ajreynol

2014-08-08	Add draft of BV proof signature (incomplete) and example proof.	ajreynol