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

Age	Commit message (Collapse)	Author
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-09-18	Support a personal build configuration and make rules.	Morgan Deters

2013-09-13	Move some regress benchmarks around that took too long, other test cleanup.	Morgan Deters

2013-04-03	Some final minor changes before cutting 1.1.	Morgan Deters
	* update documentation * update the cut-release script * spelling/wording updates * add a (previously-failing) fuzzer regression
2013-04-01	Fixes for two bugs:	Morgan Deters
	* one that Tim found in model generation for records containing Booleans * another that the fuzzer found in quantifiers + check-models Test cases enabled/added for both.
2013-01-28	some fixes for win32, including ability to "make check" win32 builds via wine	Morgan Deters

2012-12-03	Fix for fuzzer-found model bug	Clark Barrett

2012-11-26	Removing DioSolver::acceptableOriginalNodes(). This assertion was too ↵	Tim King
	strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.
2012-11-25	Adding a regression test from bug 462.	Tim King

2012-11-19	Adding hand minimized test for bug 450.	Tim King

2012-11-15	More fixes to model generation, with previously failing testcases	Clark Barrett
	Also refactored some header file includes to reduce compile time
2012-11-14	bug fixes to models, array rewriter with previously failing testcases	Clark Barrett

2012-08-28	fix regression tests for automake 1.11 and automake 1.12---both versions ↵	Morgan Deters
	should work now
2012-06-12	bufixes and the bugs	Dejan Jovanović
	* array now only propagates thropugh the equality engine * assertions in the equality rewriting to ensure eq -> { eq, T, F }
2012-06-12	test cases for the	Dejan Jovanović
	d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end() assertion fail
2012-06-06	Changes to the combination mechanism, lots of details. Not done yet, there ↵	Dejan Jovanović
	are still the AUFBV wrong results, but it seems better. http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
2012-05-16	testcase for bug 337	Dejan Jovanović

2012-05-15	test cases	Dejan Jovanović