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

Age	Commit message (Collapse)	Author
2018-09-22	cmake: Added regression tests and target make regress.	Aina Niemetz

2018-09-22	cmake: Added initial build infrastructure.	Aina Niemetz

2018-03-21	Move regression tests to single Makefile.am (#1658)	Andres Noetzli
	Until now, regression tests were split across tens of different Makefile.am, which required a lot of code duplication and does not really seem to be in the spirit of automake. If we want to change the LOG_COMPILER/LOG_DRIVER for example, we have to change every single Makefile.am, which is cumbersome (I was able to get something semi-working by exporting those variables but it didn't seem very clean). Additionally, it made the output of the regression tests fairly verbose and split the output across multiple log files. Finally it also limited parallelism when running the regression tests (this fix lowers the time it takes to run regression level 1 from 3m to 1m45s on my machine with 16 threads). This commit moves all the regression tests into test/regress/Makefile.tests and changes test/regress/Makefile.am to deal with this new structure. Finally, it changes how the test summary in test/Makefile.am is produced: instead of relying on the log files for the subdirectories, it greps for the test results in the log files of the individual tests. Not the most elegant solution but we should probably anyway delegate that task to a Python script at some point.
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ć