| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-02-17 | Fix strings preprocessing for justification heuristic | Morgan Deters |
| 2014-02-17 | type conversion | Tianyi Liang |
| 2014-02-13 | fix expanding def | Tianyi Liang |
| 2014-01-28 | merge internal and user of charat & substr into one | Tianyi Liang |
| 2014-01-22 | Some minor fixes to SmtEngine strings settings. | Morgan Deters |
| 2014-01-22 | add warning for using strings in ALL_SUPPORTED | Tianyi Liang |
| 2014-01-22 | Smarter options, but still have a bug | Tianyi Liang |
| 2014-01-18 | strings with new ideas | Tianyi Liang |
| 2014-01-16 | adds partial functions | Tianyi Liang |
| 2014-01-10 | Add new method --quant-cf for finding conflicts eagerly for quantified formul... | Andrew Reynolds |
| 2014-01-03 | Removing and consolidating options for uf-ss and quantifiers. Bug fix for in... | Andrew Reynolds |
| 2014-01-03 | Added support for proof production in Equality Engine. Cleaned up existing p... | Andrew Reynolds |
| 2013-12-24 | Java datatype API fixups, datatype API examples | Morgan Deters |
| 2013-12-23 | Proof-checking code; fixups of segfaults and missing functionality in proof g... | Morgan Deters |
