| Age | Commit message (Expand) | Author |
|---|
| 2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
| 2013-04-02 | Remove old README file from rewrite-rules left over from new-theory script lo... | Morgan Deters |
| 2013-04-02 | Fix get-authors script to not extract email addresses, canonicalize names, ad... | Morgan Deters |
| 2013-04-02 | One final fix to "make submission" rule | Morgan Deters |
| 2013-04-01 | update copyrights | Morgan Deters |
| 2013-04-01 | Adjust release Makefile rules, new run script | 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 | Cleaning up the demand restart code. | Tim King |
| 2013-04-01 | Adding a restart test strategy to integers. | Tim King |
| 2013-04-01 | Adding demand restart. | Tim King |
| 2013-04-01 | Adding tests for the previous commit. | Tim King |
| 2013-04-01 | Merging some cleanup work: | Morgan Deters |
| 2013-04-01 | Fix for iff terms over equalities between the same term and differing constants. | Tim King |
| 2013-04-01 | Fix bug 491 and related issues with checkModel() and quantifiers. Enabling p... | Morgan Deters |
| 2013-04-01 | fixed TheoryBool rewriter bug | lianah |
| 2013-04-01 | fixed bug 502; now the core bv solver only gives the model for variables and ... | lianah |
| 2013-03-30 | changed option to run inequality solver by default | Liana Hadarean |
| 2013-03-30 | Disabling eager array index splitting for QF_AUFLIA | Clark Barrett |
| 2013-03-30 | do simple ite rewriting within quantifiers | Andrew Reynolds |
| 2013-03-29 | make Boolean term conversion partially non-recursive (resolves bug 501) | Morgan Deters |
| 2013-03-29 | Merge branch 'master' of github.com:CVC4/CVC4 | Dejan Jovanović |
| 2013-03-29 | removing cryptominisat since we're not using it | Dejan Jovanović |
| 2013-03-28 | fix memory corruption in arrays destructor | Morgan Deters |
| 2013-03-27 | some Java bindings fixes (fixes Debian build problems) | Morgan Deters |
| 2013-03-27 | Fixed a warning, made eager-index default to true (better for QF_AUFBV) | Clark Barrett |
| 2013-03-27 | Fixed bug in arrays | Clark Barrett |
| 2013-03-27 | Added assertion | Clark Barrett |
| 2013-03-27 | Updates to model-based array solver | Clark Barrett |
| 2013-03-27 | New model-based array procedure | Clark Barrett |
| 2013-03-27 | reverted the core solver to do static slicing, added option --bv-core-solver | lianah |
| 2013-03-27 | fixed inequality checkDisequalities inefficiency | lianah |
| 2013-03-27 | Merge branch 'master' into bv-core | lianah |
| 2013-03-27 | fixed some model stuff | lianah |
| 2013-03-27 | fixed model generation bug; commented out attempt at inequality propagation | lianah |
| 2013-03-26 | inequality solver now only splits on disequalities when complete | lianah |
| 2013-03-26 | added model generation for bv subtheories and bv-inequality solver option | lianah |
| 2013-03-26 | Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac | Morgan Deters |
| 2013-03-26 | Make --incremental the default when running interactively | Morgan Deters |
| 2013-03-26 | core theory currently disabled | lianah |
| 2013-03-26 | getModelValue implementation in bitvectors | Dejan Jovanović |
| 2013-03-26 | adding | Dejan Jovanović |
| 2013-03-26 | Merge branch 'master' of git@github.com:CVC4/CVC4.git | Dejan Jovanović |
| 2013-03-26 | moving bv before arrays | Dejan Jovanović |
| 2013-03-26 | fixed inequality bugs due to improper explanation | lianah |
| 2013-03-25 | cleaned up the bv subtheory interface; added check for inequality theory comp... | lianah |
| 2013-03-25 | java input stream adapters working | Morgan Deters |
