summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers
AgeCommit message (Expand)Author
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
2020-08-11Fix unsupported option in regress1. (#4874)Andrew Reynolds
2020-07-14Fix regression output. (#4741)Andrew Reynolds
2020-07-13Debug instantiations output (#4739)Andrew Reynolds
2020-07-13Statistics on instantiations per quantified formula. (#4719)Andrew Reynolds
2020-07-09Ensure legal elimination for witness rewrite (#4688)Andrew Reynolds
2020-07-02Fix regression option (#4680)Andrew Reynolds
2020-06-30Simplify quantifiers strategy for when to apply last call effort check with f...Andrew Reynolds
2020-06-17Do not traverse WITNESS for partial substitutions in extended rewriter (#4630)Andrew Reynolds
2020-04-22Convert V2.5 SMT regressions to V2.6. (#4319)Abdalrhman Mohamed
2020-04-20Make option names related to CEGQI consistent (#4316)Andrew Reynolds
2020-04-14Disable preregistration of instantiations for cegqi in incremental (#4251)Andrew Reynolds
2020-04-14Remove a few spurious assertions (#4294)Andrew Reynolds
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-03-23Simplify auxiliary variable handling in CEGQI (#4141)Andrew Reynolds
2020-03-13Remove regress for real to int (#4071)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback