summaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2015-04-23A few more minor updates to match google repository with CVC4 repositoryClark Barrett
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-03-10CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf sig...ajreynol
2014-08-20Update bv proof signature and example, after discussions with Liana.ajreynol
2014-08-08Add draft of BV proof signature (incomplete) and example proof.ajreynol
2014-05-23Fix bug in E-matching Real/Int terms.Andrew Reynolds
2014-05-16lfsc_checker: fix some warnings reported by _both_ gcc and clangKshitij Bansal
2014-03-19Fix proof signatures makefileMorgan Deters
2014-03-19Fix a memory leak in LFSC proof checker. Largest QF_UF proof from Morgan (pr...Andrew Reynolds
2014-03-14dos2unix on the proof signatures, and fix the makefile.Morgan Deters
2014-03-13Add working example of LFSC proof with quantifiers. Update quantifiers signa...Andrew Reynolds
2014-03-12Work on array pf signature, add working example. Add quantifiers proof signa...Andrew Reynolds
2014-01-03Added support for proof production in Equality Engine. Cleaned up existing p...Andrew Reynolds
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-18Reduce autoconf version for dependence (should fix 32-bit builds).Morgan Deters
2013-12-16First attempt at incorporating LFSC proof checker into CVC4.Morgan Deters
2013-10-03Adding example proof signatures for LFSC.Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback