Age | Commit message (Expand) | Author |
2014-11-07 | Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor impr... | ajreynol |
2014-11-07 | Revert "Fix missing case in model postprocessor (resolves bug #595)." | Morgan Deters |
2014-11-07 | Merge branch '1.4.x' | Morgan Deters |
2014-11-07 | Fix missing case in model postprocessor (resolves bug #595). | Morgan Deters |
2014-10-28 | Preprocessing step for finding finite runs of well-defined function definitio... | ajreynol |
2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters |
2014-10-16 | Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor ch... | ajreynol |
2014-10-14 | Context-dependent expr attributes are now attached to a specific SmtEngine, a... | Morgan Deters |
2014-10-11 | Merge branch '1.4.x' | Morgan Deters |
2014-10-11 | Some defensive programming at destruction time, and fix a latent dangling poi... | 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-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 |