Age | Commit message (Expand) | Author |
2013-04-23 | Theory "alternates" support | Morgan Deters |
2013-04-18 | making sure sat context is zero when user context is popped to 0 in SmtEngine... | lianah |
2013-04-18 | fixing destruction order in SmtEngine | lianah |
2013-04-03 | * changing the bitblast-eager to bitblast on pre-register | Dejan Jovanović |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-04-01 | update copyrights | Morgan Deters |
2013-04-01 | Fix regression error by turning off model-based solver when models are on | Clark Barrett |
2013-04-01 | Turning on model based array solver for QF_AX | Clark Barrett |
2013-04-01 | Made eager lemmas an option, enabled for QF_AX | Clark Barrett |
2013-04-01 | Disabling eager array index splitting for QF_AX | Clark Barrett |
2013-04-01 | Fixes for two bugs: | Morgan Deters |
2013-04-01 | Merging some cleanup work: | Morgan Deters |
2013-04-01 | Fix bug 491 and related issues with checkModel() and quantifiers. Enabling p... | Morgan Deters |
2013-03-30 | Disabling eager array index splitting for QF_AUFLIA | Clark Barrett |
2013-03-29 | make Boolean term conversion partially non-recursive (resolves bug 501) | Morgan Deters |
2013-03-26 | Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac | Morgan Deters |
2013-03-22 | Support for Boolean term conversion in datatypes. | Morgan Deters |
2013-03-21 | Some model and printing fixes for defined functions in input. | Morgan Deters |
2013-03-21 | Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException | Morgan Deters |
2013-03-20 | Some statistics for narrowing down incrementality issues (push/pop vs solve t... | Morgan Deters |
2013-03-19 | Fixes for miplib-trick application (and a new testcase) | Morgan Deters |
2013-03-15 | Boolean terms rewriting for quantified variables of type Bool, when quantifie... | Morgan Deters |
2013-03-14 | Merge branch '1.0.x' | Morgan Deters |
2013-03-14 | fix to build system: #include the proper file when they are in both builds an... | Morgan Deters |
2013-03-11 | ite removal option for quantifiers --ite-remove-quant, e-matching for boolean... | Andrew Reynolds |
2013-03-05 | Merge branch '1.0.x' | Morgan Deters |
2013-03-05 | Bugfix for SmtEngine: proper unsubscribing for NodeManager events | Morgan Deters |
2013-03-01 | Merge branch '1.0.x' | Morgan Deters |
2013-02-26 | Fix for quantifiers containing Boolean terms. | Morgan Deters |
2013-02-24 | added option --model-u-dt-enum for outputting uninterpreted sorts as datatype... | Andrew Reynolds |
2013-02-20 | Some exception specification fixes in SmtEngine/Command infrastructure | Morgan Deters |
2013-02-16 | Some cleanup and copyright updating | Morgan Deters |
2013-02-12 | Fix a preprocessing performance issue. | Morgan Deters |
2013-02-07 | Merge branch '1.0.x' | Morgan Deters |
2013-02-07 | Significant work on bug #491 (not yet closed). | Morgan Deters |
2013-02-05 | Fix to miplib trick to make it less "cautious" and apply in more cases | Morgan Deters |
2013-02-04 | Some fixes for the miplib preprocessing pass. | Morgan Deters |
2013-02-04 | Model no longer adds subterms of quantifiers to equality engine, this fixed b... | Andrew Reynolds |
2013-02-03 | Some cleanup of miplib regressions and options | Morgan Deters |
2013-02-03 | new option for doing top-level miplib substitutions (or not) | Morgan Deters |
2013-02-03 | extended miplib trick to 6 vars, should work on pp miplib examples now | Morgan Deters |
2013-02-03 | new miplib pass, works for 1 or 2 vars | Morgan Deters |
2013-01-27 | some fixes for Intel benchmarks regarding quantifiers and datatypes, datatype... | Andrew Reynolds |
2013-01-27 | some fixes for Intel benchmarks regarding quantifiers and datatypes, datatype... | Andrew Reynolds |
2013-01-25 | fix --check-model --finite-model-find when used together (related to bug 486) | Morgan Deters |
2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters |
2013-01-25 | fix --check-model --finite-model-find when used together (related to bug 486) | Morgan Deters |
2013-01-24 | Add win32 support (merge from mdeters/win32, with some cleanup). | Morgan Deters |
2012-12-11 | SMT-LIB compliance fix to get-assignment; resolves bug 480 | Morgan Deters |
2012-12-01 | Fix the way abstract values are typed; fixes some compliance issues. | Morgan Deters |