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

Age	Commit message (Collapse)	Author
2018-04-02	a formula should be an instance of itself (#1668)	yoni206
	Proof checking failed when applying the instantiation rule so that the original formula and the instantiated formula are the same. Fixed using the new "ifequal" construct in lfsc.
2017-01-04	Marking the proof signature files as non-executable.	Tim King

2016-05-02	Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ↵	ajreynol
	do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
2014-03-14	dos2unix on the proof signatures, and fix the makefile.	Morgan Deters

2014-03-13	Add working example of LFSC proof with quantifiers. Update quantifiers ↵	Andrew Reynolds
	signature to avoid dependent types in side condition.
2014-03-12	Work on array pf signature, add working example. Add quantifiers proof ↵	Andrew Reynolds
	signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.