Age | Commit message (Expand) | Author |
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-09 | Disallow copy/assignment of SmtEngine. | Morgan Deters |
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-28 | Add option to avoid dumping partial models/proofs. | Andrew Reynolds |
2014-05-27 | Some fixes to GC order in Java. | Morgan Deters |
2014-05-26 | Separating an implicit inclusion of smt_engine.h from theory.h. | Tim King |
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-14 | Add initial support for co-datatypes. | Andrew Reynolds |
2014-04-10 | Fix the build; --check-proof works for UF but not for the new UFC logic. | Morgan Deters |
2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for in... | Andrew Reynolds |
2014-04-10 | Boolean terms conversion fix for datatypes, fixes a problem Andy discovered o... | Morgan Deters |
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-04 | For security, add --no-filesystem-access option, which disables SMT-LIB scrip... | Morgan Deters |
2014-04-03 | Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiann... | Morgan Deters |
2014-03-20 | Merge pull request #22 from kbansal/sets-model | Kshitij Bansal |
2014-03-20 | cleanup | Kshitij Bansal |
2014-03-19 | Refactor the theory specific parts of definition expansion into the theory so... | Martin Brain |
2014-03-19 | Set dumping options from (set-option..) and API more directly. | Morgan Deters |
2014-03-11 | Fix for (get-assignment), resolves bug 553. | Morgan Deters |
2014-03-11 | Merge branch '1.3.x' | Morgan Deters |
2014-03-11 | Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok. | 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-03-04 | Guard java-specific swig code with SWIGJAVA. | Thomas Hunger |
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 |