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

Age	Commit message (Collapse)	Author
2013-11-11	Change exit status to be more consistent with other command-line tools: 0 ↵	Morgan Deters
	success, nonzero error
2012-10-06	* Fix some regressions' expected outputs.	Morgan Deters
	* Ensure Rewriter::init() is called before ::rewrite(). The array type enumerator recently gave us an end-run around ::init(). TheoryEngine no longer calls these, they're done via static initialization. * Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-25	some buggy examples for incrementality, and make bug326 run as part of make ↵	Morgan Deters
	regress, because the bug was fixed. Also make QuantifiersModule's destructor virtual (it has virtual members). (this commit was certified error- and warning-free by the test-and-commit script.)