| Age | Commit message (Expand) | Author |
|---|
| 2014-09-30 | Proofs- and cores-related segfault fixes (mainly a usability issue), thanks C... | Morgan Deters |
| 2014-09-16 | Refactoring of conjecture generator. Determine subgoals are non-canonical ba... | ajreynol |
| 2014-09-03 | Implement and enable --dt-var-exp-quant, cleanup trace messages, minor change... | ajreynol |
| 2014-08-29 | Do not use pure theory terms as single triggers. Minor cleanup. | ajreynol |
| 2014-08-26 | Bug fixes for --purify-triggers, --dt-force-assignment. | ajreynol |
| 2014-08-23 | Unsat core printing. | Morgan Deters |
| 2014-08-23 | Some fixes for dump- and get-unsat-core. | Morgan Deters |
| 2014-08-22 | One small thing forgotten in core commit. | 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-08-15 | Update smt_engine.cpp | Kshitij Bansal |
| 2014-07-12 | Fix a bug in Boolean terms and arrays. Thanks to Jean-Christophe Filliatre f... | Morgan Deters |
| 2014-07-01 | Update copyrights. | Morgan Deters |
| 2014-06-25 | Turn strings-exp off by default (for the release) | Morgan Deters |
| 2014-06-23 | Fatal error if --unconstrained-simp and --produce-models used together (befor... | Morgan Deters |
| 2014-06-19 | added model generation to eager bit-blasting and turned abc off by default | lianah |
| 2014-06-19 | New translator features: expand define-funs and combine assertions. | 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-14 | Evil bitvector preprocessing pass for simplifying powers of two. | lianah |
| 2014-06-13 | Fix handling of ALIA. | ajreynol |
| 2014-06-11 | Some clean-up, post bv-merge. | Morgan Deters |
| 2014-06-10 | Merging Tim's pseudoboolean work from his fmcad14 branch. | Tim King |
| 2014-06-10 | Merging CAV14 paper bit-vector work. | lianah |
| 2014-06-06 | Sets translate, and other short fixes | Kshitij Bansal |
| 2014-06-04 | SmtEngine::checkModel() now checks that model values are of the correct type ... | Morgan Deters |
| 2014-05-15 | Minor fixes. Add SMTCOMP 2014 script. | Andrew Reynolds |
| 2014-05-14 | Finish --dump-instantiations option. Update scripts. | Andrew Reynolds |
| 2014-05-13 | Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ... | ajreynol |
| 2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ... | Andrew Reynolds |
| 2014-05-10 | Bug fixes to CBQI. Add first draft of CASC j7 TFF script. Add regression, m... | Andrew Reynolds |
| 2014-05-09 | Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC... | Andrew Reynolds |
| 2014-05-02 | Add option --dt-stc-ind for strengthening skolemization. Refactor skolemizat... | Andrew Reynolds |
| 2014-04-30 | T-entailment work, and QCF (quant conflict find) work that uses it. | Tim King |
| 2014-04-10 | Add support for cardinality constraints logic UFC. Add regressions in fmf/. ... | Andrew Reynolds |
| 2014-04-09 | fix get-info error-behavior | Kshitij Bansal |
| 2014-04-03 | Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiann... | Morgan Deters |
| 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 |
| 2014-03-11 | Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu... | Andrew Reynolds |
| 2014-03-07 | Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodi... | Morgan Deters |
| 2014-03-07 | Fix bug 554 (nominally). | Morgan Deters |
| 2014-03-07 | Fix strings-exp setting. | Morgan Deters |
| 2014-02-28 | a new regular expression engine for solving both positive and negative member... | Tianyi Liang |
| 2014-02-21 | portfolio: fix export of emptyset | Kshitij Bansal |
| 2014-02-20 | Fix ite and iff handling in QCF. Add option for heuristic instantiation in Q... | Andrew Reynolds |
| 2014-02-18 | switch to total function str.to.int: maps invalid and non-digit strings to 0 | Tianyi Liang |
| 2014-02-17 | bring back the commits which is lost accidentally. | Tianyi Liang |
| 2014-02-17 | add str2int | Tianyi Liang |
| 2014-02-17 | Fix for strings-exp: enable quantifiers | Morgan Deters |
