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

Age	Commit message (Collapse)	Author
2016-11-17	Fix Makefiles in test	Andres Notzli
	With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that.
2013-12-23	Proof-checking code; fixups of segfaults and missing functionality in proof ↵	Morgan Deters
	generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but not --check-proofs, since LFSC code uses globals) * proofs are not yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-11-11	Change exit status to be more consistent with other command-line tools: 0 ↵	Morgan Deters
	success, nonzero error
2013-09-18	Support a personal build configuration and make rules.	Morgan Deters

2013-04-17	boolean flatten: bug fix in dfs search	Kshitij Bansal
	(this is not intended to (and doesn't) address the issue with NodeBuilder limit)
2013-04-16	generalize to handle and	Kshitij Bansal

2013-04-16	flatten or nodes	Kshitij Bansal

2013-01-28	some fixes for win32, including ability to "make check" win32 builds via wine	Morgan Deters

2012-08-28	fix regression tests for automake 1.11 and automake 1.12---both versions ↵	Morgan Deters
	should work now
2012-04-18	add the missing BINARY variable in some test/regress makefiles	Kshitij Bansal

2012-04-05	Support to test the "dumper" mechanism in regressions (feeding dump output ↵	Morgan Deters
	back in) by doing "make regress RUN_REGRESSION_ARGS=--dump"
2011-10-29	support for proof regressions in other parts of the test tree	Morgan Deters

2011-07-05	missing test case	Dejan Jovanović

2011-07-05	updated preprocessing and rewriting input equalities into inequalities for LRA	Dejan Jovanović