summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers
AgeCommit message (Expand)Author
2020-06-06Fix destruction order in NodeManager (#4578)Andres Noetzli
2020-06-05Skip parse-error regression for comp builds (#4567)Andres Noetzli
2020-06-03Do not apply unconstrained simplification when quantifiers are present (#4532)Andrew Reynolds
2020-06-02Fix scope issue with pulling ITEs in extended rewriter. (#4547)Andrew Reynolds
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
2020-05-19Do not eliminate variables that are equal to unevaluatable terms (#4267)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-16SyGuS instantiation quantifiers module (#3910)Mathias Preiner
2020-04-15Do not normalize to representatives for variable equalities in conflict-based...Andrew Reynolds
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-03-18Fix issue with multiple infinities in CEGQI for LIRA (#4114)Andrew Reynolds
2020-03-06Remove tester name from APIs (#3929)Andrew Reynolds
2020-02-28Replace conditional rewrite pass in quantifiers with the extended rewriter (#...Andrew Reynolds
2020-02-08Make "unknown" non-critical for unsat cores check (#3728)Andres Noetzli
2019-09-04Remove duplicate regression tests. (#3227)Mathias Preiner
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
2019-04-16Minor simplifications to theory quantifiers (#2953)Andrew Reynolds
2018-11-05Increasing coverage (#2683)yoni206
2018-09-24Fix quantifiers selector over store rewrite (#2510)Andrew Reynolds
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-06Refactor and document quantifiers variable elimination and conditional splitt...Andrew Reynolds
2018-09-04Make quantifiers strategies exit immediately when in conflict (#2099)Andrew Reynolds
2018-08-20Remove support for *.expect files in regressions (#2341)Andres Noetzli
2018-08-07Fix inference of pre and post conditions for non variable arguments. (#2237)Andrew Reynolds
2018-06-01Fix quantified bv variable elimination (#2039)Andrew Reynolds
2018-06-01 Use monomial sum utility to solve for quantifiers macros (#2038)Andrew Reynolds
2018-05-22Set same options for proofs as for unsat cores (#1957)Andres Noetzli
2018-04-25Fix issue with multi-triggers that include variable triggers (#1810)Andrew Reynolds
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
2018-03-19Enable CEGQI for non-linear (#1674)Andrew Reynolds
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
2018-01-03Global negate (#1466)Andrew Reynolds
2017-12-20Fixes for cbqi-bv (#1449)Andrew Reynolds
2017-12-20Add explicit disequality handling when generating side condition for CBQI BV....Aina Niemetz
2017-12-08Fixed side conditions for CBQI BV, added unit tests. (#1434)Aina Niemetz
2017-11-21Cegqi bv remove extract terms preprocess pass (#1376)Andrew Reynolds
2017-11-15Reenable some regressions, minor. (#1369)Andrew Reynolds
2017-11-14Clean Ceg Instantiators (#1365)Andrew Reynolds
2017-11-01CBQI BV choice expressions (#1296)Andrew Reynolds
2017-10-25CBQI BV: Add handling for missing operators. (#1274)Aina Niemetz
2017-10-23CBQI BV: Add ULT/SLT inverse handling. (#1268)Aina Niemetz
2017-10-13CBQI BV: Added EXTRACT handling. (#1240)Aina Niemetz
2017-10-12CBQI BV quick heuristics (#1239)Andrew Reynolds
2017-10-12Initial support for solving bit-vector inequalities (#1229)Andrew Reynolds
2017-10-11Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)Aina Niemetz
2017-10-11Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)Mathias Preiner
2017-10-11Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback