summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers
AgeCommit message (Expand)Author
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
2020-12-22Make theory preprocess rewrite equalities a preprocessing pass (#5711)Andrew Reynolds
2020-12-22Remove preregister instantiation heuristic (#5713)Andrew Reynolds
2020-12-17Simplify and fix check models (#5685)Andrew Reynolds
2020-12-15Remove bv divide by zero option (#5672)Andrew Reynolds
2020-12-10Refactor regressions (#5639)Andrew Reynolds
2020-12-07Fix and reenable fact vs lemma optimization in datatypes (#5614)Andrew Reynolds
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-11-30More fixes for quantifier elimination (#5533)Andrew Reynolds
2020-11-25Add regressions for closed issues (#5526)Andrew Reynolds
2020-11-20Fix remove term formula policy for terms beneath quantifiers (#5497)Andrew Reynolds
2020-11-20Support nested quantifier elimination for get-qe command (#5490)Andrew Reynolds
2020-11-19Enable new implementation of CEGQI based on nested quantifier elimination (#5...Andrew Reynolds
2020-11-19Use new let binding utility in smt2 printer (#5472)Andrew Reynolds
2020-11-19Fix issues related to eliminating extended arithmetic operators (#5475)Andrew Reynolds
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
2020-09-22Allow E-matching by default when strings are enabled (#5117)Andrew Reynolds
2020-09-14Fix needsModel method for CEGQI (#5048)Andrew Reynolds
2020-09-01[API] Fix Python Examples (#4943)Andres Noetzli
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-08-19Require `--strings-exp` when using `str.substr` (#4916)Andres Noetzli
2020-08-19[Regressions] Do not test `--check-proofs` anymore (#4914)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback