projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
add bag.fold operator (#7718)
[cvc5.git] / test / regress / CMakeLists.txt
2021-08-30 Andrew ReynoldsFix quantifiers dynamic split module for parametric... blob | commitdiff | raw
2021-08-26 Mathias Preinerint2bv: Fix conversion of signed bit-vector values... blob | commitdiff | raw | diff to current
2021-08-23 Andrew ReynoldsPurify substitutions in strings proof reconstruction... blob | commitdiff | raw | diff to current
2021-08-23 Andrew ReynoldsGeneralize inequality elimination in quantifiers rewrit... blob | commitdiff | raw | diff to current
2021-08-23 Andrew ReynoldsFix single invocation partition for higher-order (... blob | commitdiff | raw | diff to current
2021-08-22 Andrew ReynoldsPrenex quantified formulas with user annotations by... blob | commitdiff | raw | diff to current
2021-08-20 Andrew ReynoldsSupport sygus standard command syntax set-feature ... blob | commitdiff | raw | diff to current
2021-08-17 Andrew ReynoldsFix policy for eliminating quantified formulas (#7017) blob | commitdiff | raw | diff to current
2021-08-09 Andrew V. JonesCreate grouping of tests that exercise '--use-approx... blob | commitdiff | raw | diff to current
2021-08-05 Andrew ReynoldsFix policy for rewriting string equalities (#6916) blob | commitdiff | raw | diff to current
2021-08-04 Andrew ReynoldsFix policy for merging subproofs (#6981) blob | commitdiff | raw | diff to current
2021-07-30 Gereon KremerAllow changing certain options while solving (#6945) blob | commitdiff | raw | diff to current
2021-07-29 Andrew ReynoldsIntegrate central equality engine approach into theory... blob | commitdiff | raw | diff to current
2021-07-27 Andres NoetzliAdd regression for fixed `str.indexof_re` issue (#6938) blob | commitdiff | raw | diff to current
2021-07-23 Aina NiemetzFP: Add option to word-blast more lazily. (#6904) blob | commitdiff | raw | diff to current
2021-07-22 Andres NoetzliAdd support for minimal unsat cores (#4605) blob | commitdiff | raw | diff to current
2021-07-14 Haniel Barbosa[proof] Fix open proof issues in SAT proof (#6887) blob | commitdiff | raw | diff to current
2021-07-14 Andrew ReynoldsFix for context on input proof generator (#6873) blob | commitdiff | raw | diff to current
2021-07-13 Haniel Barbosa[rewriter] Add rewrite to order IFF (equality for Boole... blob | commitdiff | raw | diff to current
2021-07-12 Andrew ReynoldsFix for learned rewrite pass, add regression (#6850) blob | commitdiff | raw | diff to current
2021-07-09 Andrew ReynoldsFix sets cardinality inference involving equivalent... blob | commitdiff | raw | diff to current
2021-07-07 Haniel Barbosa[unsat cores] Adding regressions from #4971 (#6852) blob | commitdiff | raw | diff to current
2021-07-05 Andres Noetzli[Strings] Fix incorrect rewrite (#6837) blob | commitdiff | raw | diff to current
2021-07-02 Mathias PreinerFix bv assert input reset assertions (#6820) blob | commitdiff | raw | diff to current
2021-07-02 Andrew ReynoldsFix rewriter for negative constant seq.nth (#6827) blob | commitdiff | raw | diff to current
2021-07-01 Andrew ReynoldsAdd recursive function definitions to subsolver in... blob | commitdiff | raw | diff to current
2021-06-30 Mathias PreinerUse SAT context level for --bv-assert-input instead... blob | commitdiff | raw | diff to current
2021-06-30 yoni206pow2: new test (#6819) blob | commitdiff | raw | diff to current
2021-06-30 Andrew ReynoldsDo not apply fmfBound to standard quantifiers when... blob | commitdiff | raw | diff to current
2021-06-30 Andrew ReynoldsFix pre vs. post-rewrite in proofs for theory preproces... blob | commitdiff | raw | diff to current
2021-06-30 yoni206int-to-bv: correct model values (#6811) blob | commitdiff | raw | diff to current
2021-06-28 yoni206Rewrite POW to POW2 when the base is 2 (#6806) blob | commitdiff | raw | diff to current
2021-06-26 yoni206pow2 -- final changes (#6800) blob | commitdiff | raw | diff to current
2021-06-24 Andrew ReynoldsFix linear arithmetic for duplicate lemmas in increment... blob | commitdiff | raw | diff to current
2021-06-23 Haniel Barbosa[hol] Disable bound fmf when HOL (#6792) blob | commitdiff | raw | diff to current
2021-06-23 Haniel Barbosa[regressions] Adding regression from #5371 (#6791) blob | commitdiff | raw | diff to current
2021-06-23 Haniel Barbosa[parser] [hol] Fix parser check for allowing functions... blob | commitdiff | raw | diff to current
2021-06-22 Andrew ReynoldsAlways check legal eliminations in quantified logics... blob | commitdiff | raw | diff to current
2021-06-22 Andrew ReynoldsFix type enumeration for non first-class sorts in FMF... blob | commitdiff | raw | diff to current
2021-06-21 Mathias PreinerFix model issues with --bitblast=eager. (#6753) blob | commitdiff | raw | diff to current
2021-06-10 Andrew ReynoldsEnsure bv2nat and int2bv are not rewritten when using... blob | commitdiff | raw | diff to current
2021-06-09 Andres NoetzliMake `--solve-int-as-bv=X` robust to rewriting (#6722) blob | commitdiff | raw | diff to current
2021-06-09 Andres NoetzliReorder ITE rewrites (#6723) blob | commitdiff | raw | diff to current
2021-06-08 Andrew ReynoldsFix for 2 dimensional dependent bounded quantifiers... blob | commitdiff | raw | diff to current
2021-06-08 Gereon KremerFix statistics option handler (#6703) blob | commitdiff | raw | diff to current
2021-06-08 Andrew ReynoldsFix str.update reduction (#6696) blob | commitdiff | raw | diff to current
2021-06-07 Andrew Reynolds(proof-new) Fix missing connection in trust substitutio... blob | commitdiff | raw | diff to current
2021-06-05 Andres NoetzliRemove unwanted side effects in `SPLIT_EQ_STRIP_L`... blob | commitdiff | raw | diff to current
2021-06-04 Mathias Preinerbv: Enable bitblast solver by default. (#6660) blob | commitdiff | raw | diff to current
2021-06-04 Andres NoetzliFix handling of start index in `str.indexof_re` (#6674) blob | commitdiff | raw | diff to current
2021-06-02 Andrew ReynoldsFix unsat core proofs (#6655) blob | commitdiff | raw | diff to current
2021-06-02 Andres NoetzliMake `STRINGS_CTN_DECOMPOSE` an explicit conflict ... blob | commitdiff | raw | diff to current
2021-06-02 Gereon KremerFix issues with double negation in circuit propagator... blob | commitdiff | raw | diff to current
2021-06-01 Andrew ReynoldsDisable timeout regressions (#6650) blob | commitdiff | raw | diff to current
2021-05-31 Andres NoetzliCompute model values for nested sequences in order... blob | commitdiff | raw | diff to current
2021-05-28 Andres Noetzli`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts ... blob | commitdiff | raw | diff to current
2021-05-27 Andrew ReynoldsFix regular expression aggressive elim (#6627) blob | commitdiff | raw | diff to current
2021-05-27 Andres NoetzliFix `str.replace_re` and `str.replace_re_all` (#6615) blob | commitdiff | raw | diff to current
2021-05-27 Andrew ReynoldsFix CEGQI for datatypes with Boolean subfields (#6630) blob | commitdiff | raw | diff to current
2021-05-27 Andrew ReynoldsFix spurious assertion for trivial abduction (#6629) blob | commitdiff | raw | diff to current
2021-05-27 Andres NoetzliReturn `REWRITE_AGAIN` after rewriting bvcomp (#6624) blob | commitdiff | raw | diff to current
2021-05-27 Andrew ReynoldsEnable new justification heuristic by default (#6613) blob | commitdiff | raw | diff to current
2021-05-24 Andrew ReynoldsFix non-fixed length case in re-elim (#6612) blob | commitdiff | raw | diff to current
2021-05-24 Andrew ReynoldsFix re-elim length requirement for symbolic RE membersh... blob | commitdiff | raw | diff to current
2021-05-20 Aina NiemetzFix echo printing. (#6573) blob | commitdiff | raw | diff to current
2021-05-19 Andrew ReynoldsPass empty vector when constructing re empty, fixes... blob | commitdiff | raw | diff to current
2021-05-19 Haniel BarbosaAdding regressions that failed on old unsat cores ... blob | commitdiff | raw | diff to current
2021-05-19 Andrew ReynoldsFix positive contains indexof rewrites for empty string... blob | commitdiff | raw | diff to current
2021-05-19 Andres NoetzliImprove handling of `:named` attributes (#6549) blob | commitdiff | raw | diff to current
2021-05-18 Andres NoetzliFix `collectEmptyEqs()` in string utils (#6562) blob | commitdiff | raw | diff to current
2021-05-17 Andres NoetzliFix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites... blob | commitdiff | raw | diff to current
2021-05-12 Andrew ReynoldsEnsure sequences of Booleans generate Boolean term... blob | commitdiff | raw | diff to current
2021-05-08 Andrew ReynoldsAdd support for datatype update (#6449) blob | commitdiff | raw | diff to current
2021-05-07 Aina NiemetzMove slow regressions and update guidelines. (#6508) blob | commitdiff | raw | diff to current
2021-05-06 Andrew ReynoldsDiscard duplicate terms in patterns (#6501) blob | commitdiff | raw | diff to current
2021-05-04 Aina NiemetzFP: Move removal of generic to_fp operations to rewrite... blob | commitdiff | raw | diff to current
2021-05-03 Aina NiemetzFP: Rewrite to_fp conversion from signed bit-vector... blob | commitdiff | raw | diff to current
2021-05-03 Aina NiemetzSymFPU: Automatically apply patch from 2020-11-14.... blob | commitdiff | raw | diff to current
2021-04-27 Andrew ReynoldsMove slow regression to regress3 (#6451) blob | commitdiff | raw | diff to current
2021-04-27 Andrew ReynoldsFix refutational soundness bug in quantifier prenexing... blob | commitdiff | raw | diff to current
2021-04-24 Andrew ReynoldsImprove getValue for non-evaluated operators (#6436) blob | commitdiff | raw | diff to current
2021-04-21 Mathias PreinerGoodbye CVC4, hello cvc5! (#6371) blob | commitdiff | raw | diff to current
2021-04-20 Andrew ReynoldsAdd instantiation pool feature to the API (#6358) blob | commitdiff | raw | diff to current
2021-04-15 Aina Niemetzpreprocessing context: Add wrapper for model substituti... blob | commitdiff | raw | diff to current
2021-04-15 Andrew ReynoldsReenable regression for minimizing instantiations ... blob | commitdiff | raw | diff to current
2021-04-14 Abdalrhman MohamedMerge equivalent sub-obligations instead of discarding... blob | commitdiff | raw | diff to current
2021-04-13 Andrew ReynoldsRefactor quantifiers macros (#6348) blob | commitdiff | raw | diff to current
2021-04-13 Abdalrhman MohamedFix sexpr bug with AST output language. (#6329) blob | commitdiff | raw | diff to current
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) blob | commitdiff | raw | diff to current
2021-04-09 Andrew ReynoldsAdd regressions for issue 6214 (#6305) blob | commitdiff | raw | diff to current
2021-04-09 Andres NoetzliLearn equalities involving Boolean variables (#6323) blob | commitdiff | raw | diff to current
2021-04-08 Andrew ReynoldsAdd benchmark for issue 5101 (#6301) blob | commitdiff | raw | diff to current
2021-04-08 Andrew ReynoldsAdd benchmark for issue 4400 (#6288) blob | commitdiff | raw | diff to current
2021-04-08 Andrew ReynoldsInitial support for parametric datatypes in sygus ... blob | commitdiff | raw | diff to current
2021-04-07 Andrew ReynoldsAdd benchmark for 6270 (#6283) blob | commitdiff | raw | diff to current
2021-04-07 Haniel Barbosa[proof-new] Fixing SMT post-processor's handling of... blob | commitdiff | raw | diff to current
2021-04-07 Andrew ReynoldsAdd benchmark for issue 4420 (#6286) blob | commitdiff | raw | diff to current
2021-04-06 Andrew ReynoldsAdd benchmark for issue 5942 (#6296) blob | commitdiff | raw | diff to current
2021-04-06 Andrew ReynoldsFix tptp parser for negative rational (#6297) blob | commitdiff | raw | diff to current
2021-04-06 Andrew ReynoldsFix issue with lemma during equality engine iterator... blob | commitdiff | raw | diff to current
next