| Age | Commit message (Expand) | Author |
|---|
| 2016-06-20 | Fixed a bug where the proofManager's init() call was not getting called, resu... | Guy |
| 2016-06-08 | Support for printing a global let map in LFSC proofs. | Guy |
| 2016-06-03 | Better infrastructure for proving constant disequality. | Guy |
| 2016-06-03 | A better mechanism for handling BV terms with aliases: inject the alias at th... | Guy |
| 2016-06-02 | Fixed a magical bug that only appears when compiling with clang: | Guy |
| 2016-06-02 | Fix | Guy |
| 2016-06-01 | Merge from proof branch | Guy |
| 2016-06-01 | Revert "Merging proof branch" | Guy |
| 2016-06-01 | Merging proof branch | Guy |
| 2016-04-30 | Reviewed Tim's Asan changes and improved SatProof comments. | Liana Hadarean |
| 2016-04-26 | Fixing memory leaks for garbage collection of ResChains in the sat proof impl... | Tim King |
| 2016-04-20 | update from the master | PaulMeng |
| 2016-04-09 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
| 2016-04-09 | Made ProofArray's printing functions non-static, and consequently the data me... | Guy |
| 2016-04-03 | Updating the copyright headers and scripts. | Tim King |
| 2016-04-03 | s_ prefix for static members | Guy |
| 2016-04-03 | Removed the theory-specific merge reason types. Instead, added a mechanism fo... | Guy |
| 2016-03-23 | squash-merge from proof branch | Guy |
| 2016-02-24 | Adding the missing clause_id.h file. | Tim King |
| 2016-02-24 | Unifying the definitions of ClauseId to a single source of truth. | Tim King |
| 2016-02-02 | Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ... | Tim King |
| 2016-02-01 | Adding a destructor to ProofOutputChannel. | Tim King |
| 2016-02-01 | Fixing white spaces in sat_proof.h. | Tim King |
| 2016-02-01 | Deleting the dead code in proof/sat_proof.cpp. | Tim King |
| 2016-01-28 | Adding listeners to Options. | Tim King |
| 2016-01-26 | Merged bit-vector and uf proof branch. | Liana Hadarean |
| 2015-12-30 | Shuffling around public vs. private headers | Tim King |
| 2015-12-24 | Miscellaneous fixes | Tim King |
| 2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
| 2015-10-26 | This commit fixes a bug related to a public header depending on a compiler fl... | Tim King |
| 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 |
