| Age | Commit message (Expand) | Author |
|---|
| 2015-06-01 | When proof enabled, disable uf sym break. Add regression. | ajreynol |
| 2015-05-25 | Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report. | ajreynol |
| 2015-05-12 | Merge pull request #74 from finnhaedicke/namespace_minisat | barrettcw |
| 2015-04-23 | Added option for --check-unsat-cores and various core bug fixes (merge of Mor... | Liana Hadarean |
| 2015-04-17 | moved Minisat namespace into CVC4 | Finn Haedicke |
| 2015-03-16 | Fixed proof unitialized memory and minor memory leaks. | Liana Hadarean |
| 2015-03-10 | CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf sig... | ajreynol |
| 2014-08-25 | Fix Win32 builds. | Morgan Deters |
| 2014-08-22 | Unsat core infrastruture and API (SMT-LIB compliance to come). | Morgan Deters |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-06-21 | Fix compiler warnings (mostly unused variables). | Morgan Deters |
| 2013-12-24 | Java datatype API fixups, datatype API examples | Morgan Deters |
| 2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
| 2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters |
| 2013-11-13 | Add virtual destructors where missing | Morgan Deters |
| 2013-11-10 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters |
| 2013-11-05 | fixed proof regression script and added a new uf test case | lianah |
| 2013-10-09 | cleaned up proof code | lianah |
| 2013-10-09 | fixed uf proof bug: now storing deleted theory lemmas | lianah |
| 2013-10-08 | added currying for uf proofs; still needs debugging | lianah |
| 2013-10-08 | fixed uf proof with holes bugs | lianah |
| 2013-10-07 | fixed some bugs | Liana Hadarean |
| 2013-10-07 | first draft implementation of uf proofs with holes | Liana Hadarean |
| 2013-09-13 | Fix sat_proof "parentheses into the void" after conferring with Liana. | Morgan Deters |
| 2013-05-10 | now proofs print mapping between atom and propositional variable as a comment... | lianah |
| 2013-05-10 | fixes to the proof system so it works with theory lemmas and explanations | lianah |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2013-03-14 | Merge branch '1.0.x' | Morgan Deters |
| 2013-03-14 | fix to build system: #include the proper file when they are in both builds an... | Morgan Deters |
| 2013-02-16 | Some cleanup and copyright updating | Morgan Deters |
| 2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-09-28 | rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak... | Morgan Deters |
| 2012-09-24 | Fix the memout issue seen in recent nightly regressions (was due to a | Morgan Deters |
| 2012-09-15 | minor interface improvements, compliance fixes | Morgan Deters |
| 2012-08-03 | fix for proofs-enabled builds | Morgan Deters |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-07 | Various fixes to documentation---typos, some incomplete documentation fixed, ... | Morgan Deters |
| 2011-11-01 | Improvements to header installation on user machines. Internally, we can | Morgan Deters |
| 2011-10-29 | fix some doxygen warnings | Morgan Deters |
| 2011-10-29 | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::g... | Morgan Deters |
| 2011-10-28 | * ability to output NodeBuilders without first converting them to Nodes---use... | Morgan Deters |
| 2011-10-28 | merged the proofgen3 branch into trunk: | Liana Hadarean |
