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

Age	Commit message (Collapse)	Author
2020-06-16	Update copyright headers.	Aina Niemetz

2019-03-26	Update copyright headers.	Aina Niemetz

2018-06-25	Updated copyright headers.	Aina Niemetz

2017-10-25	Switching EqProof to use shared_ptr everywhere. (#1217)	Tim King
	This clarifies the memory ownership of EqProofs.
2017-07-07	Update copyright headers.	Mathias Preiner

2016-09-16	In a ROW guard proof, if the transitivity proof does not have a disequality, ↵	guykatzz
	we can deduce that it is a constant-disequality proof and process it accordingly
2016-09-16	Handling a corner case where a ROW's guard is a constant disequality.	Guy
	If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality
2016-07-06	A few proof bugs fixed	Guy

2016-06-01	Merge from proof branch	Guy

2016-06-01	Revert "Merging proof branch"	Guy
	This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01	Merging proof branch	Guy

2016-04-03	Updating the copyright headers and scripts.	Tim King

2016-04-03	Removed the theory-specific merge reason types. Instead, added a mechanism ↵	Guy
	for dynamically allocating these tags upon request.
2016-03-24	Refactored the equality engine in order to remove theory-specific logic from ↵	Guy
	equality path reconstruction