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

Age	Commit message (Collapse)	Author
2014-11-08	Fix bug with incremental+datatypes. Minor cleanup. Disable regression ↵	ajreynol
	bug484, enable parsing_ringer.
2014-11-07	Properly distinguish which EQC to assign values in datatypes, use ↵	ajreynol
	assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure.
2014-10-06	Extended parsing testcase, with constant arrays and RESET.	Morgan Deters

2014-10-06	Merge branch '1.4.x'	Morgan Deters
	Conflicts: test/regress/regress0/arrays/Makefile.am
2014-10-06	Fix native language parsing of chained-store expressions (resolves bug 585). ↵	Morgan Deters
	Thanks to Eric Seidel for the report. Also fixed some operator precedence problems w.r.t. store expressions and arithmetic.
2014-10-04	Enable some old bug testcases that (maybe?) never got added.	Morgan Deters

2014-10-03	Add some (so far trivial) regressions for constant arrays.	Morgan Deters

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-08-28	fix regression tests for automake 1.11 and automake 1.12---both versions ↵	Morgan Deters
	should work now
2012-05-14	Fixed assertion failures in array theory	Clark Barrett
	This fixes bugs 335 and 333.
2012-04-18	add the missing BINARY variable in some test/regress makefiles	Kshitij Bansal

2012-04-11	merge from arrays-clark branch	Morgan Deters

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-12	forgot to reflect naming change in makefile. fixed	Morgan Deters

2011-07-12	fix bug 272, array unsoundness, and some array cleanup	Morgan Deters

2011-07-11	remove some array regressions from "make check" so nightly regressions run	Morgan Deters

2011-07-11	status of examples	Morgan Deters

2011-07-11	new array bugs ?	Morgan Deters

2011-07-11	mark the new minimized benchmark as unsat	Morgan Deters

2011-07-11	if running in QF_AX, equalities over terms of uninterpreted sort go to ↵	Morgan Deters
	arrays, as well as pre-registration of free constants of uninterpreted sort, etc..
2011-07-11	minimized example	Morgan Deters

2011-07-11	array benchmarks	Morgan Deters

2011-05-23	Merge from arrays2 branch.	Morgan Deters