| Age | Commit message (Expand) | Author |
|---|
| 2016-10-12 | Fix some typos, fix some formatting, minor cleanupfix_typos | Andres Notzli |
| 2016-10-11 | Merge branch 'origin' of https://github.com/CVC4/CVC4.git | Paul Meng |
| 2016-10-05 | Added an option that allow empty dependencies when attempting to minimize pre... | guykatzz |
| 2016-09-27 | Removing an unused iterator. | Tim King |
| 2016-09-16 | Let arith_proof print its own terms | Guy |
| 2016-08-24 | Merge remote-tracking branch 'origin/master' | PaulMeng |
| 2016-08-11 | Add support for fewer preprocessing holes | Andres Notzli |
| 2016-08-09 | Fix missing/redundant spaces in proofsfix_proof_spaces | Andres Notzli |
| 2016-08-05 | Minor: add/fix comments, remove redundant includes | Andres Notzli |
| 2016-08-03 | Fixed an issue where arrays proofs would sometimes have an extra ")" at the end. | Guy |
| 2016-07-28 | The "aggressive" optimizer for lemma L now returns the conjunction of all lem... | Guy |
| 2016-07-28 | Bug fix involving negated lemmas | Guy |
| 2016-07-27 | Proper handling of IFF lemmas in the unsat core. | Guy |
| 2016-07-27 | Added an option for a more aggressive weakest implicant optimization | Guy |
| 2016-07-27 | If we can't find a weaker implicant, fail gracefully and return the original ... | Guy |
| 2016-07-26 | Fix warnings in src/proof | Andres Notzli |
| 2016-07-26 | Bug fix: | Guy |
| 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 |
