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

Age	Commit message (Collapse)	Author
2014-04-06	Reduced example from pcc's bug report.	Tim King

2014-03-12	Some standardization of regression Makefiles that got out of sync. Fixes ↵	Morgan Deters
	cases of nonterminating rewrite-rules regressions.
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-01-28	some fixes for win32, including ability to "make check" win32 builds via wine	Morgan Deters

2012-11-13	added support for division by zero for bit-vector division operators	Liana Hadarean

2012-08-28	fix regression tests for automake 1.11 and automake 1.12---both versions ↵	Morgan Deters
	should work now
2012-06-16	changing theoryOf in shared mode with arrays to move equalities to arrays	Dejan Jovanović
	disabled in bitvectors due to non-stably infinite problems the option to enable it is --theoryof-mode=term
2012-06-06	also remove now-incorrect comment from makefile	Morgan Deters

2012-06-06	Fixed broken test case, removed one that is a mistake	Clark Barrett

2012-06-06	unconstrained regressions are now run with "make check", but with ↵	Morgan Deters
	--unconstrained-simp option
2012-06-06	Fixing numerous issues with tests and "make dist":	Morgan Deters
	* test/regress/regress0/unconstrained wasn't being distributed. This caused the debian build failure last night. (It still doesn't run on "make check", but had to be distributed properly.) * Fixing an issue where a test name was longer than 99 characters and couldn't be distributed in the "old" tar format. (Told automake to use a newer tar format.)
2012-06-04	Added preprocessing pass that propagates unconstrained values - solves all of	Clark Barrett
	the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help generally on at least BV and maybe others. Off by default for now - results are mixed and it's hard to evaluate with so many existing assertion failures and segfaults - will re-evaluate once those are fixed