Age | Commit message (Expand) | Author |
2016-08-25 | Minor cleanup preprocessing, add ppNotifyAssertions. | ajreynol |
2016-08-25 | Options for counterexample guided instantiation. | ajreynol |
2016-08-19 | Fixed two bugs | Clark Barrett |
2016-08-19 | Added fitsSignedLong and fitsUnsignedLong | Clark Barrett |
2016-08-16 | Initial infrastructure for ExtTheory, generalize extended term handling in Th... | ajreynol |
2016-08-15 | Expression sharing on demand in LFSC (replace definitionally equivalent child... | ajreynol |
2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for bounde... | ajreynol |
2016-08-12 | Add a few more regressions. | ajreynol |
2016-08-12 | Minor fixes to model construction to take singleton equivalence classes into ... | ajreynol |
2016-08-12 | Merge pull request #90 from 4tXJ7f/fewer_preproc_holes | guykatzz |
2016-08-11 | Add support for fewer preprocessing holes | Andres Notzli |
2016-08-11 | Minor change to strings, introduce proxy vars only when necessary. | ajreynol |
2016-08-10 | Improvements to strings: work on propagations for reverse normal form process... | ajreynol |
2016-08-09 | Merge pull request #89 from 4tXJ7f/fix_proof_spaces | guykatzz |
2016-08-09 | Fixes for sep star rewrite. | ajreynol |
2016-08-09 | Fix missing/redundant spaces in proofsfix_proof_spaces | Andres Notzli |
2016-08-05 | Merge pull request #88 from 4tXJ7f/fix_comments | guykatzz |
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-08-03 | Merge pull request #87 from 4tXJ7f/fix_oob_access | barrettcw |
2016-07-30 | Prioritize inferences when processing normal forms in strings. | ajreynol |
2016-07-28 | The "aggressive" optimizer for lemma L now returns the conjunction of all lem... | Guy |
2016-07-28 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-28 | Bug fix involving negated lemmas | Guy |
2016-07-28 | Fix bug 749. | ajreynol |
2016-07-28 | Add the negative conjunction case | Guy |
2016-07-27 | Fix out-of-bounds access in ExprManager | Andres Notzli |
2016-07-27 | Proper instrumentation of the preprocessing phase | Guy |
2016-07-27 | proper handling of ITEs | 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 | Merge pull request #86 from 4tXJ7f/fix_warnings | guykatzz |
2016-07-26 | Fix warnings in src/proof | Andres Notzli |
2016-07-26 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-26 | Bug fix: | Guy |
2016-07-26 | Add option to minimize sygus solutions based on using weakest implicants of i... | ajreynol |
2016-07-26 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-26 | Letification of BV constants | Guy |
2016-07-26 | Minor improvements to strings related to constant splitting, including a few ... | ajreynol |
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-25 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy |
2016-07-24 | cleanup | Guy |
2016-07-24 | Use letification for the aliasing declarations as well (consequently, print t... | Guy |
2016-07-24 | Proper handling for lemmas that are conjuncts: | Guy |
2016-07-22 | Minor, error handling for polymorphism + sep logic. | ajreynol |
2016-07-21 | Fixes for strings, explanations for constant split propagations, substr under... | ajreynol |