summaryrefslogtreecommitdiff
path: root/test/regress/regress2
AgeCommit message (Expand)Author
2021-07-27Add regression for fixed `str.indexof_re` issue (#6938)Andres Noetzli
2021-07-01Add recursive function definitions to subsolver in sygus (#6824)Andrew Reynolds
2021-06-16Make symfpu a required dependency. (#6749)Aina Niemetz
2021-06-11Better support for HOL parsing and set up (#6697)Haniel Barbosa
2021-06-10Ensure bv2nat and int2bv are not rewritten when using solve-bv-as-int (#6725)Andrew Reynolds
2021-06-04Fix handling of start index in `str.indexof_re` (#6674)Andres Noetzli
2021-06-03Renaming pow2 to p2 in regression tests (#6675)yoni206
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-05-28Disable `--jh-rlv-order` for slow regressions (#6633)Andres Noetzli
2021-05-27Fix `str.replace_re` and `str.replace_re_all` (#6615)Andres Noetzli
2021-05-27Enable new justification heuristic by default (#6613)Andrew Reynolds
2021-05-21Fix tests of unsat cores (#6593)Andrew Reynolds
2021-05-19Change the default unsat cores (#6571)Haniel Barbosa
2021-05-18Fix `collectEmptyEqs()` in string utils (#6562)Andres Noetzli
2021-05-17Improve integration of CAD with nl-Ext (#6542)Gereon Kremer
2021-05-07Move slow regressions and update guidelines. (#6508)Aina Niemetz
2021-05-06Discard duplicate terms in patterns (#6501)Andrew Reynolds
2021-04-27Move slow regression to regress3 (#6451)Andrew Reynolds
2021-04-25More check models (#6439)Andrew Reynolds
2021-04-24Improve getValue for non-evaluated operators (#6436)Andrew Reynolds
2021-04-22Fix models for sygus-inference, bv2int, real2int (#6421)Andrew Reynolds
2021-04-22Reconciling proofs and unsat cores (#6405)Haniel Barbosa
2021-03-16[proof-new] Renaming proof option to be in sync with SMT-LIB (#6154)Haniel Barbosa
2021-03-16[proof-new] Disabling proofs on regressions with known bug (#6151)Haniel Barbosa
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-01-20SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)Aina Niemetz
2020-12-17Simplify and fix check models (#5685)Andrew Reynolds
2020-12-10Refactor regressions (#5639)Andrew Reynolds
2020-12-08Add regression from #1978. (#5552)Gereon Kremer
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-12-01Add regressions from #3687. (#5553)Gereon Kremer
2020-12-01Add regressions for #4707. (#5555)Gereon Kremer
2020-11-23Change UF ho to ppRewrite instead of expand definition (#5499)Andrew Reynolds
2020-11-10Do not mark extended functions as reduced based on decomposing contains (#5407)Andrew Reynolds
2020-11-09Do not regress explanations of datatype lemmas (#5376)Andrew Reynolds
2020-10-14bv2int: implementing the iand-sum mode (#5265)yoni206
2020-10-13bv2int: rewritings and unsat cores (#5263)yoni206
2020-10-06bv-to-int: change order of passes (#5208)yoni206
2020-09-23bv2int: new options for bvand translation (#5096)yoni206
2020-09-15bv2int: support models in tests (#5068)yoni206
2020-09-09bv2int: improvement in lazy failures (#5020)yoni206
2020-09-03Changing the handled operators in bv2int preprocessing pass (#4970)yoni206
2020-08-28Incremental support for bv_to_int (#4967)yoni206
2020-08-24Increase regress level to 2 for production build. (#4888)Mathias Preiner
2020-08-19[Regressions] Do not test `--check-proofs` anymore (#4914)Andres Noetzli
2020-07-12Add support for string/sequence update (#4725)Andrew Reynolds
2020-07-11Changing bv_to_int options (#4721)yoni206
2020-07-09Disable unsat cores in timeout regression (#4713)Andrew Reynolds
2020-06-10Add support for str.replace_re/str.replace_re_all (#4594)Andres Noetzli
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback