summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers
AgeCommit message (Expand)Author
2021-10-20Add regressions for fixed issues (#7421)Andrew Reynolds
2021-10-20Reimplement support for relational triggers (#7063)Andrew Reynolds
2021-10-15Add more regressions for fixed issues (#7382)Andrew Reynolds
2021-10-14Add regression for fixed issue (#7365)Andrew Reynolds
2021-09-22Remove CVC language support (#7219)Mathias Preiner
2021-09-02Disable sygus-inst for regression close to time limit. (#7122)Aina Niemetz
2021-09-02Enable sygus-inst for FP, NIA and NRA. (#7098)Aina Niemetz
2021-08-22Prenex quantified formulas with user annotations by default (#7048)Andrew Reynolds
2021-07-29[proofs] Set BV solver to better proof-producing one when proofs on (#6903)Haniel Barbosa
2021-07-29Integrate central equality engine approach into theory engine, add option and...Andrew Reynolds
2021-07-27Revert change to regression (#6940)Andrew Reynolds
2021-07-27Minor changes from proof-new (#6937)Andrew Reynolds
2021-07-07Fix regressions for competition build (#6846)Andrew Reynolds
2021-07-03Add output tags -o, --output. (#6826)Mathias Preiner
2021-06-30Do not apply fmfBound to standard quantifiers when only stringsExp is enabled...Andrew Reynolds
2021-06-22Always check legal eliminations in quantified logics (#6720)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-03Renaming pow2 to p2 in regression tests (#6675)yoni206
2021-06-02Remove redundant logic ALL_SUPPORTED. (#6664)Aina Niemetz
2021-05-27Enable new justification heuristic by default (#6613)Andrew Reynolds
2021-05-21Fix tests of unsat cores (#6593)Andrew Reynolds
2021-05-07Move slow regressions and update guidelines. (#6508)Aina Niemetz
2021-04-30Use substitutions for implementing defined functions (#6437)Andrew Reynolds
2021-04-27Fix refutational soundness bug in quantifier prenexing (#6448)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-20Add instantiation pool feature to the API (#6358)Andrew Reynolds
2021-04-15Reenable regression for minimizing instantiations (#6367)Andrew Reynolds
2021-04-08Add benchmark for issue 4400 (#6288)Andrew Reynolds
2021-04-07Add benchmark for issue 4420 (#6286)Andrew Reynolds
2021-04-05Add benchmark for issue 4412 (#6287)Andrew Reynolds
2021-04-05Enable UF when pre-skolem nested option is enabled (#6282)Andrew Reynolds
2021-03-30Implement simple tracking of instantiation lemmas (#6077)Andrew Reynolds
2021-03-23Removing unused build options and deprecated proof compile flag (#6195)Haniel Barbosa
2021-03-16ci: Enable checking of proofs + unsat cores. (#6088)Mathias Preiner
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-10Add quant elim regression (#6103)Andrew Reynolds
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-02-25Move slow regressions to regress1 (#5999)Andrew Reynolds
2021-02-09[quantifiers] Fix prenex computation (#5879)Haniel Barbosa
2021-01-30Fix unguarded call to get representative (#5838)Andrew Reynolds
2021-01-28Always theory-preprocess lemmas (#5817)Andrew Reynolds
2021-01-26Remove deprecated quantifiers modules (#5820)Andrew Reynolds
2021-01-25Ensure uses of ground terms in triggers are preprocessed and registered (#5808)Andrew Reynolds
2021-01-20Fix corner case of wrongly applied selector as trigger (#5786)Andrew Reynolds
2021-01-20SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)Aina Niemetz
2020-12-22Move slow regression to regress3 (#5715)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback