| Age | Commit message (Expand) | Author |
|---|
| 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-08-01 | Make --fmf-fun and --macros-quant work in incremental mode. Add regressions. | ajreynol |
| 2015-07-31 | Sygus support for inductive datatypes. | ajreynol |
| 2015-04-23 | Added option for --check-unsat-cores and various core bug fixes (merge of Mor... | Liana Hadarean |
| 2015-01-26 | Output solutions for synthesis conjectures with --dump-synth. Minor refactor... | ajreynol |
| 2014-11-17 | Resource-limiting work. | Liana Hadarean |
| 2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters |
| 2014-10-14 | Context-dependent expr attributes are now attached to a specific SmtEngine, a... | Morgan Deters |
| 2014-10-06 | Support for RESET command in CVC native language (and infrastructure for supp... | Morgan Deters |
| 2014-08-22 | Unsat core infrastruture and API (SMT-LIB compliance to come). | Morgan Deters |
| 2014-08-18 | Add support for quantifier-specific instantiation levels. Add option for set... | ajreynol |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-06-19 | Fix for new CASC features, fixes Java builds. | Morgan Deters |
| 2014-06-19 | For casc : print models of functions rewritten by sort inference. | ajreynol |
| 2014-06-09 | Disallow copy/assignment of SmtEngine. | Morgan Deters |
| 2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ... | Andrew Reynolds |
| 2014-05-09 | Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC... | Andrew Reynolds |
| 2014-03-20 | Merge pull request #22 from kbansal/sets-model | Kshitij Bansal |
| 2014-03-20 | cleanup | Kshitij Bansal |
| 2014-03-19 | Refactor the theory specific parts of definition expansion into the theory so... | Martin Brain |
| 2014-03-11 | Fix for (get-assignment), resolves bug 553. | Morgan Deters |
| 2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
| 2013-12-16 | First attempt at incorporating LFSC proof checker into CVC4. | Morgan Deters |
| 2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters |
| 2013-09-09 | Fix declare-datatypes dumping bug (bug 385). | Morgan Deters |
| 2013-09-09 | Support per-command verbosity settings. | Morgan Deters |
| 2013-09-05 | Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a se... | Morgan Deters |
| 2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters |
| 2013-07-06 | Model output is now const; this related to bug 519 | Morgan Deters |
| 2013-05-20 | Don't allow get-model & co after a user push/pop | Morgan Deters |
| 2013-05-20 | Better error on invalid logic strings. | Morgan Deters |
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2013-03-22 | Support for Boolean term conversion in datatypes. | Morgan Deters |
| 2013-02-20 | Some exception specification fixes in SmtEngine/Command infrastructure | Morgan Deters |
| 2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters |
| 2012-12-01 | Adding SmtEngine::setLogic(const char* logic) so that smt.setLogic("QF_LRA");... | Tim King |
| 2012-11-27 | Functions and predicates over Boolean now work with --check-models and output... | Morgan Deters |
| 2012-11-27 | Tuples and records merge. Resolves bug 270. | Morgan Deters |
| 2012-11-26 | don't include internal variables in model output | Morgan Deters |
| 2012-11-17 | * Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT... | Morgan Deters |
| 2012-11-12 | Fix for bug 444, dealing with the placing of set-logic in dumping modes. | Morgan Deters |
| 2012-11-09 | Bug-fix for a crash involving improperly-thrown exceptions; also, add LogicEx... | Morgan Deters |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 2012-10-10 | Abstract values for SMT-LIB. | Morgan Deters |
| 2012-10-09 | * make Model class private (as discussed at meeting today) | Morgan Deters |
| 2012-10-05 | Bug-related: | Morgan Deters |
| 2012-10-05 | BoolExpr removed and replaced with Expr | Dejan Jovanović |
| 2012-10-04 | Implemented array type enumerator, more fixes for models | Clark Barrett |
