Age | Commit message (Expand) | Author |
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 |
2017-03-09 | better proof support for bools and formulas | guykatzz |
2017-03-07 | More fixes for printing/parsing sets, fix kind name. | ajreynol |
2017-03-07 | Fix cvc parser for set compliment. | ajreynol |
2017-03-06 | Support for set compliment and universe set. Simplify approach for sep.nil no... | ajreynol |
2017-03-03 | Fix for collectModelInfo related to finite types + preregistration. Generaliz... | ajreynol |
2017-03-03 | Another minor fix for sets related to sharing + finite element types. | ajreynol |
2017-03-02 | Fixes related to sets. | ajreynol |
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
2017-02-07 | Generalize finite bound inference to unifiable variables in set membership li... | ajreynol |
2017-01-30 | Fix regexp cache issue in strings, add regression. | ajreynol |
2017-01-18 | Fix non-idempotent rewrite in Array rewriter | Andres Noetzli |
2017-01-11 | Merge pull request #129 from timothy-king/regression-scrubber | Clark Barrett |
2017-01-11 | Fix for when variables are (partially) bound in multiple ways, add regression... | ajreynol |
2017-01-10 | Adding regression test scrubbing. | Tim King |
2017-01-05 | Disabling a regression test that assumes CVC4 is configured with proofs on. M... | Tim King |
2017-01-04 | Fix for tff type declarations inTPTP parser, fixes bug 748. Other minor chan... | ajreynol |
2017-01-04 | Marking regression test files as non-executable. | Tim King |
2017-01-04 | Reverting two files encoding with DOS linebreaks back into using unix linebre... | Tim King |
2016-12-16 | Fix dependency tracing for fewerPreprocessingHoles | Andres Notzli |
2016-12-12 | Fix split-find-unsat-w-emp test | Andres Notzli |
2016-12-08 | Fix (inactive) `MultSlice` rewrite | Andres Notzli |
2016-12-08 | Enable remaining cardinality benchmarks | ajreynol |
2016-12-07 | Add missing regression | ajreynol |