Age | Commit message (Expand) | Author |
2017-05-31 | Fix model construction for BV with cbqi. Minor change to defaults. | ajreynol |
2017-05-31 | Minor change to defaults, update smt comp script, minor changes to options in... | ajreynol |
2017-05-26 | Checking that equalities belong to the arithmetic theory in the solve() routine. | Tim King |
2017-05-20 | Fix bug 812. | ajreynol |
2017-05-15 | Cleanup handling of division (possible fix for bugs 803, 804, 805). | ajreynol |
2017-05-15 | Merge pull request #158 from 4tXJ7f/fix_sets_rewriter | Andrew Reynolds |
2017-05-15 | Fix minor bug in sets rewriter | Andres Noetzli |
2017-05-15 | Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802. | ajreynol |
2017-05-13 | Fix out-of-bounds access in test | Andres Notzli |
2017-05-12 | Make signal handlers safer | Andres Notzli |
2017-05-10 | Do not split on cardinality for string equivalence classes with non-constant ... | ajreynol |
2017-05-09 | Change str.replace for empty string. | ajreynol |
2017-05-05 | Do not eliminate extended arithmetic symbols when finite model finding is on,... | ajreynol |
2017-04-28 | Minor fixes | ajreynol |
2017-04-28 | Fix bug for real division. | ajreynol |
2017-04-28 | Do not eliminate non-standard arithmetic operators in recursive function defi... | ajreynol |
2017-04-24 | Fixes and simplifications for fmf mbqi. | ajreynol |
2017-04-24 | Fix parsing selectors for nullary constructors in smtlib 2.6 format. | ajreynol |
2017-04-23 | Changing spaces to tabs in Makefile. | Tim King |
2017-04-21 | Disabled bug639.smt2 which still fails. | Clark Barrett |
2017-04-21 | Add test cases for bugs 639 and 681. | Clark Barrett |
2017-04-21 | Fix new relations regressions to use sets-ext. | ajreynol |
2017-04-21 | Handle subtypes in sets. Bug fixes for tuples with subtypes. | ajreynol |
2017-04-20 | Support for relational operators identity and join image | Paul Meng |
2017-04-19 | Fixes for handling set universe: restrict upwards rule for universe to member... | ajreynol |
2017-04-14 | Actively split for upwards closusure intersection. Minor clean up, add regres... | ajreynol |
2017-04-14 | Fix for fmf-fun when the option is set by user command. | ajreynol |
2017-04-07 | Change option names for nl. | ajreynol |
2017-04-05 | Merge pull request #143 from FabianWolff/master | Clark Barrett |
2017-04-05 | Fix bug 698. | ajreynol |
2017-04-05 | Caching for fun def process, add regression. | ajreynol |
2017-04-05 | Remove extraneous portion of an nl regression. | ajreynol |
2017-04-05 | Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NON... | ajreynol |
2017-04-05 | Fix several spelling errors | Fabian Wolff |
2017-04-04 | Enable multi-trigger-linear by default, add option. | ajreynol |
2017-04-04 | Do not solve for 0-ary non-constant symbols (for which isVar returns true), a... | ajreynol |
2017-04-02 | Adding a model based axiom instantiation scheme for multiplication. Merge com... | Tim King |
2017-03-28 | Refactor the standard effort of relational solver | Paul Meng |
2017-03-28 | Fix bug 787. | ajreynol |
2017-03-28 | Fix for bug 733 | Clark Barrett |
2017-03-24 | Add some regressions. Minor. | ajreynol |
2017-03-22 | Minor fix for bounded integers. | ajreynol |
2017-03-20 | fixed cvc4 parser for set complement | Paul Meng |
2017-03-17 | better support for proof production when encountering bool terms: handle the ... | guykatzz |
2017-03-16 | More fixes, features to examples. | ajreynol |
2017-03-16 | Minor fixes, always expand applications of lambdas at preprocess. | ajreynol |
2017-03-16 | Support for SMT LIB 2.6 syntax declare-datatype and match. | ajreynol |
2017-03-16 | Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ... | ajreynol |
2017-03-15 | Fix regress1 Makefile for rewriterules, fixes bug 783. | ajreynol |
2017-03-15 | Allow 0 argument recursive functions. Fixes bug 782. | ajreynol |