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

Age	Commit message (Collapse)	Author
2021-03-25	Deleting old LFSC signatures (#6194)	Haniel Barbosa

2021-03-09	Update copyright headers to 2021. (#6081)	Aina Niemetz

2020-09-22	Update copyright header script to support CMake and Python files (#5067)	Mathias Preiner
	This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-08-17	Add identifier name for side condition. (#4902)	Alex Ozdemir
	``` (! sc (^ ...) ^ this is the identifier! ``` We require that side-conditions have an identifier. We usually provide this identifier, but in this one case we did not. The old lexer accepted the side condition without the identifier. The new one does not.
2020-07-20	Fix a deadlock in the signature tests. (#4772)	Alex Ozdemir
	* wait() deadlocks if the OS pipe fills * communicate() does not This is essentially a duplicate of [this](https://github.com/CVC4/LFSC/pull/38).
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