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

Age	Commit message (Collapse)	Author
2016-10-21	Move slow regress0 benchmarks to regress1, increment regress1 through regress3.	ajreynol

2014-02-09	More complete guess instantiation strategy, cvc4 now typically times out ↵	Andrew Reynolds
	instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
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-09-13	Move some regress benchmarks around that took too long, other test cleanup.	Morgan Deters

2013-08-26	bug 374 fix: assert litVal=desiredVal only for leaf nodes1.2.x	Kshitij Bansal

2013-08-26	Bug 374 benchmarks	Kshitij Bansal

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

2012-09-18	SMT-LIBv2 compliance regarding outputting "unknown".	Morgan Deters
	Thanks to Peter Collingbourne for the report, and the patch! (this commit was certified error- and warning-free by the test-and-commit script.)
2012-08-28	fix regression tests for automake 1.11 and automake 1.12---both versions ↵	Morgan Deters
	should work now
2012-07-27	Minor cleanup after today's commits:	Morgan Deters
	* change some uses of "std::cout" to "Message()" * change some files to use Unix newlines instead of DOS newlines * fix compiler warning
2012-07-16	now passes "make distcheck", which does important checks for the release ↵	Morgan Deters
	(e.g., "make dist" produces a distribution that passes "make dist" and "make check", "make uninstall" actually uninstalls, "make distclean" actually cleans, ...)
2012-06-17	enabling theoryof=term for quantifiers with sharing	Dejan Jovanović
	disableing one test case in equantifiers/decision that runs long
2012-06-17	Fix array bug causing incorrect answers	Clark Barrett

2012-06-16	Adding the failing QF_AUFLIA regression mentioned in last commit.	Kshitij Bansal
	pp-regfile.delta02.smt is the one to look at with --decision=justificaiton, the delta minimized version of pp-regfile, which also gives wrong answer. due to various commits/fixes, delta01 gives correct answer currently.
2012-06-15	one bug fixed	Kshitij Bansal

2012-06-14	add failing regression, move error up	Kshitij Bansal

2012-06-14	bug fixes in justification heuristic	Kshitij Bansal
	* remove assert iteSkolemMap gives ite-s (not true with repeatSimp) * handle a corner case in findSplitter triggered by repeatSimp
2012-06-14	enabling fixed bug345 case	Dejan Jovanović

2012-06-14	fix quantifier non-bug	Kshitij Bansal

2012-06-14	failing quantifier	Kshitij Bansal

2012-06-14	add passing regression	Kshitij Bansal

2012-06-13	add passing regression	Kshitij Bansal

2012-06-13	enable some decision regressions	Kshitij Bansal

2012-06-13	decision regressions, all but one fail	Kshitij Bansal