| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-01-04 | Marking the proof signature files as non-executable. | Tim King | |
| 2016-08-05 | Minor: add/fix comments, remove redundant includes | Andres Notzli | |
| 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-03-23 | squash-merge from proof branch | Guy | |
| 2016-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean | |
| 2014-03-14 | dos2unix on the proof signatures, and fix the makefile. | Morgan Deters | |
| 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. | |||
| 2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing ↵ | Andrew Reynolds | |
| proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup. | |||
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback