Age | Commit message (Expand) | Author |
2014-10-07 | Refactor quantifiers attributes. | ajreynol |
2014-10-06 | Merge branch '1.4.x' | Morgan Deters |
2014-10-06 | Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report. | Morgan Deters |
2014-10-06 | Support for RESET command in CVC native language (and infrastructure for supp... | Morgan Deters |
2014-10-02 | Merge branch '1.4.x'. | Morgan Deters |
2014-10-02 | Fix comment in SmtEngine. | Morgan Deters |
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-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 |