| Age | Commit message (Expand) | Author |
|---|
| 2012-08-29 | * Numerous documentation fixes (fix doxygen warnings, add missing documentati... | Morgan Deters |
| 2012-08-28 | Improved compatibility layer, now supports quantifiers. Also incorporates | Morgan Deters |
| 2012-08-27 | fix a destruction-order issue that was (1) causing valgrind to complain loudl... | Morgan Deters |
| 2012-08-16 | The SmtEngine now ensures that setLogicInternal() is called even if there is ... | Morgan Deters |
| 2012-08-08 | Public interface review items: | Morgan Deters |
| 2012-08-07 | Fix SmtEngine::setInfo() handling for certain keys. This fixes the "unsuppor... | Morgan Deters |
| 2012-08-06 | Support setting :regular-output-channel and :diagnostic-output-channel. | Morgan Deters |
| 2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
| 2012-08-01 | add isFinished() to type enumerators (so we don't rely on exception-throwing ... | Morgan Deters |
| 2012-08-01 | a couple fixes to SmtEngine::setOption(). thanks Andy for the report! | Morgan Deters |
| 2012-08-01 | fix for the SmtEngine::beforeSearch() option predicate | Morgan Deters |
| 2012-07-31 | fixes for portfolio | Morgan Deters |
| 2012-07-31 | fix some file documentation | Morgan Deters |
| 2012-07-31 | Options merge. This commit: | Morgan Deters |
| 2012-07-17 | SMT-LIBv2 compliance updates: | Morgan Deters |
| 2012-07-17 | fix for --produce-models with CVC4 presentation language | Morgan Deters |
| 2012-07-16 | Support for having two SmtEngines with the same ExprManager. | Morgan Deters |
| 2012-07-12 | merged fmf-devel branch, includes support for SMT2 command get-value and (ext... | Andrew Reynolds |
| 2012-07-08 | minor SMT-LIBv2 compliance issues | Morgan Deters |
| 2012-07-08 | Bugs resolved by this commit: #314, #322, #359, #364, #365. | Morgan Deters |
| 2012-06-18 | bugfix, enable only QF_LRA, not other arith | Kshitij Bansal |
| 2012-06-18 | QF_LRA, Quantifiers: enable use decision for (only for) stopping search | Kshitij Bansal |
| 2012-06-17 | QF_AUFLIA: enable use decision for (only for) stopping search | Kshitij Bansal |
| 2012-06-17 | enabling theoryof=term for quantifiers with sharing | Dejan Jovanović |
| 2012-06-17 | Removed assertion that can fail | Clark Barrett |
| 2012-06-16 | This is an attempt to fix the bug in the justification heuristic. The | Kshitij Bansal |
| 2012-06-16 | changing theoryOf in shared mode with arrays to move equalities to arrays | Dejan Jovanović |
| 2012-06-16 | Fixing if condition for trivial equalities in arithmetic. Also some whitespac... | Tim King |
| 2012-06-15 | Fixes some assertion failures | Clark Barrett |
| 2012-06-15 | Fix for incompleteness bug with decision engine: repeated simplification | Clark Barrett |
| 2012-06-15 | one bug fixed | Kshitij Bansal |
| 2012-06-14 | WIP | Kshitij Bansal |
| 2012-06-14 | add failing regression, move error up | Kshitij Bansal |
| 2012-06-14 | New substitutions implementation - fixes performance issue seen in nonclausal | Clark Barrett |
| 2012-06-14 | Removed an assertion, unneeded header file | Clark Barrett |
| 2012-06-14 | some changes to make CVC4 work nicely with trace executor for application tra... | Morgan Deters |
| 2012-06-14 | making --simplification=none the default for quantified logics; this a reques... | Morgan Deters |
| 2012-06-14 | bug ifx, mv | Kshitij Bansal |
| 2012-06-14 | restore destruction of stuff in driver | Kshitij Bansal |
| 2012-06-14 | This commit: | Kshitij Bansal |
| 2012-06-14 | Brings the tuning branch into trunk. This includes the changes from restricte... | Tim King |
| 2012-06-12 | Moved some things around in the preprocessor. Now theory preprocessing gets | Clark Barrett |
| 2012-06-12 | cleanup of exit mechanism when decisionEngine is on\n\n fixes some bugs we we... | Kshitij Bansal |
| 2012-06-12 | Fixed compile error | Clark Barrett |
| 2012-06-12 | Enabling constant propagation | Clark Barrett |
| 2012-06-12 | Adding constant propagation code - needs more testing - off by default | Clark Barrett |
| 2012-06-09 | Turning on unconstrained simp for QF_AUFBV | Clark Barrett |
| 2012-06-08 | Merge from decision branch (till r3663) | Kshitij Bansal |
| 2012-06-07 | LogicInfo locking implemented, and some initialization-order issues in SmtEng... | Morgan Deters |
| 2012-06-06 | Don't ever call nonclausalSimplify if simplificationMode = NONE (even if | Clark Barrett |
