summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-02Add countercav2019stringsAndres Noetzli
2019-04-30fixAndres Noetzli
2019-04-30Merge branch 'master' into cav2019stringsAndres Noetzli
2019-04-30revert diffAndres Noetzli
2019-04-30Fix concat-find regexp elimination (#2983)Andres Noetzli
2019-04-30Remove stoi solve rewrite (#2985)Andrew Reynolds
2019-04-30Fix use of APPLY kind in examples (#2984)Andres Noetzli
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
2019-04-29Optimization for evaluation with unfolding (#2979)Andrew Reynolds
2019-04-25New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)Aina Niemetz
2019-04-24Fix compiler warning. (#2975)Aina Niemetz
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-04-24Dco fix (#2973)Clark Barrett
2019-04-24README: Remove project leaders, history.Aina Niemetz
2019-04-24CONTRIBUTING: Fix project leaders link.Aina Niemetz
2019-04-23[BV] An option for SAT proof optimization (#2915)Alex Ozdemir
2019-04-23Refactor normal forms in strings (#2897)Andrew Reynolds
2019-04-22Add CONTRIBUTING file. (#2968)Aina Niemetz
2019-04-18Add option to do extended rewriting preprocessing onlyAndres Noetzli
2019-04-18Fail fast strategy for propagating instances (#2939)Andrew Reynolds
2019-04-18 Less aggressive caching in equality engine when proofs are enabled (#2964)Andrew Reynolds
2019-04-17Cache explanations in the equality engine (#2937)Andrew Reynolds
2019-04-17More use of isClosure (#2959)Andrew Reynolds
2019-04-17Add rewrite for splitting equalitiesAndres Noetzli
2019-04-17mergeAndres Noetzli
2019-04-17Fix extended function decomposition (#2960)Andrew Reynolds
2019-04-16Add interface for term enumeration (#2956)Andrew Reynolds
2019-04-16Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)Andres Noetzli
2019-04-16Stratify enumerative instantiation (#2954)Andrew Reynolds
2019-04-16Minor simplifications to theory quantifiers (#2953)Andrew Reynolds
2019-04-15Check for rt library in configuration -- support for glibc<2.17 (#2854)makaimann
2019-04-15Initial version of run scripts for SMT-COMP 2019 (#2951)Andres Noetzli
2019-04-12Referring to prerelease 1.8 (#2943)Haniel Barbosa
2019-04-11 Eliminate Boolean ITE within terms, fixes 2947 (#2949)Andrew Reynolds
2019-04-09Removing references to cvc4-bugs@... (#2945)Haniel Barbosa
2019-04-08"prerelease -> release" in INSTALL (#2944)Haniel Barbosa
2019-04-08Fix email address of the bugs email list and delete obsolete RELEASE-NOTES.Aina Niemetz
2019-04-08fix copyright year in configuration file (#2942)Haniel Barbosa
2019-04-05prerelease -> release (#2941)Haniel Barbosa
2019-04-05Fix another corner case of datatypes+PBE (#2938)Andrew Reynolds
2019-04-05fix fp issue (#2940)Haniel Barbosa
2019-04-05SatClauseSetHashFunction (#2916)Alex Ozdemir
2019-04-04adding sygus news (#2934)Haniel Barbosa
2019-04-04Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)Haniel Barbosa
2019-04-03Update release notes and lib version (#2933)Haniel Barbosa
2019-04-03Update copyright headers.Aina Niemetz
2019-04-03get-authors: Add GitHub user ayveejay -> Andrew V. Jones.Aina Niemetz
2019-04-03Fix combination of datatypes + strings in PBE (#2930)Andrew Reynolds
2019-04-01FP: Fix wrong model due to partial assignment (#2910)Andres Noetzli
2019-04-01Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback