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

Age	Commit message (Collapse)	Author
2015-08-16	More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. ↵	ajreynol
	Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.
2015-08-12	Improvements to --macros-quant. Enable --clause-split by default. Bug fix ↵	ajreynol
	for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.
2014-07-01	Update copyrights.	Morgan Deters

2014-05-09	Add variable ordering to ambqi. Bug fix to macros. More preparation for ↵	Andrew Reynolds
	CASC proofs.
2014-05-08	Major simplifications to macros module.	ajreynol

2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-02-04	fixed files with DOS newlines; fixed contrib/ scripts to use git	Morgan Deters

2012-11-18	support for quantifiers macros, bug fix for bug 454 involving E-matching ↵	Andrew Reynolds
	Array select terms (thanks for the bug report Francois)
2012-11-14	replaced all static member data from rewrite rule triggers, added ↵	Andrew Reynolds
	infrastructure for recognizing quantifier macros