| Age | Commit message (Expand) | Author |
|---|
| 2016-07-26 | Letification of BV constants | Guy |
| 2016-07-26 | Added functionality to retrieve a lemma's "weakest implicant" in the unsat co... | Guy |
| 2016-07-25 | Bug fix | Guy |
| 2016-07-25 | Propagate the usage of proof let maps into constant disequality proofs | Guy |
| 2016-07-25 | Bug fix | Guy |
| 2016-07-24 | Use letification for the aliasing declarations as well (consequently, print t... | Guy |
| 2016-07-19 | Bug fix | Guy |
| 2016-07-19 | Allow a caller to query whether an unsat core is available or not | Guy |
| 2016-07-15 | Moved the assertion to a better spot | Guy |
| 2016-07-15 | The ProofManager now allows theory solvers to get their lemmas that participa... | Guy |
| 2016-07-06 | A few proof bugs fixed | Guy |
| 2016-07-05 | Merge branch 'master' of https://github.com/CVC4/CVC4.git | PaulMeng |
| 2016-07-01 | When proving a lemma, ignore literals that don't belong to the theory in ques... | Guy |
| 2016-07-01 | Handle bitvector lemmas where a literal gets rewritten into false, and conseq... | Guy |
| 2016-06-30 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
| 2016-06-30 | Support for the letification of chained AND and OR operations in LFSC proofs | Guy |
| 2016-06-23 | Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black, | Clark Barrett |
| 2016-06-20 | Addressed a bug that occurs when proof production is triggered via text flags... | Guy |
| 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 |
