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

Age	Commit message (Collapse)	Author
2014-02-09	More complete guess instantiation strategy, cvc4 now typically times out ↵	Andrew Reynolds
	instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
2013-11-11	Change exit status to be more consistent with other command-line tools: 0 ↵	Morgan Deters
	success, nonzero error
2012-09-18	SMT-LIBv2 compliance regarding outputting "unknown".	Morgan Deters
	Thanks to Peter Collingbourne for the report, and the patch! (this commit was certified error- and warning-free by the test-and-commit script.)
2012-06-11	Merge from quantifiers2-trunkmerge branch.	Morgan Deters
	Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver.