summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith
AgeCommit message (Expand)Author
2021-10-22Make CAD proofs user context dependent (#7466)Gereon Kremer
2021-09-22Remove CVC language support (#7219)Mathias Preiner
2021-09-02Implement lazy proof checking modes (#7106)Andrew Reynolds
2021-05-27Enable new justification heuristic by default (#6613)Andrew Reynolds
2021-05-21Fix tests of unsat cores (#6593)Andrew Reynolds
2021-05-17Improve integration of CAD with nl-Ext (#6542)Gereon Kremer
2021-04-25More check models (#6439)Andrew Reynolds
2021-04-24Improve getValue for non-evaluated operators (#6436)Andrew Reynolds
2021-03-24Only consider relevant terms for integer branches (#6181)Gereon Kremer
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-22(proof-new) Change proof-new option to proof (#5955)Andrew Reynolds
2021-01-20SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)Aina Niemetz
2021-01-13Do not call ppRewrite on Boolean equalities (#5762)Andrew Reynolds
2020-12-18Bugfix: proofs for props of non-normal arith lits (#5702)Alex Ozdemir
2020-12-10Refactor regressions (#5639)Andrew Reynolds
2020-12-07Do not expand theory definitions at the beginning of preprocessing (#5544)Andrew Reynolds
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
2020-10-07Make sure conflicts are not rewritten (in arithmetic) (#5219)Gereon Kremer
2020-09-17Reduce recursion in term formula removal (#5052)Andrew Reynolds
2020-08-19[Regressions] Do not test `--check-proofs` anymore (#4914)Andres Noetzli
2020-06-01Set theoryof-mode after theory widening (#4545)Andres Noetzli
2020-05-31Do not cache operator eliminations in arith (#4542)Andres Noetzli
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-03-05Remove --apply-to-const preprocessing pass (#3919)Andres Noetzli
2020-02-21Switch to th_lira.plf (#3741)Alex Ozdemir
2020-02-08Make "unknown" non-critical for unsat cores check (#3728)Andres Noetzli
2020-02-03Regression tests for arithmetic proofs. (#3701)Alex Ozdemir
2020-01-31Fix arithmetic rewriter for exponential (#3688)Andres Noetzli
2019-12-30[proof] ITE translation fix (#3484)Alex Ozdemir
2019-10-28Fix integer division rewrite (#3415)Andres Noetzli
2019-10-13Eliminate negative constant coefficients in div/mod (#2929)Andrew Reynolds
2019-10-08Make ackermannization generally applicable rather than just BV (#3315)Ying Sheng
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
2018-09-22cmake: Added regression tests and target make regress.Aina Niemetz
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-27Make division chainable in the smt2 parser (#2367)Andrew Reynolds
2018-08-20Remove support for *.expect files in regressions (#2341)Andres Noetzli
2018-08-16Refactor apply2const (#2316)Haniel Barbosa
2018-05-22Set same options for proofs as for unsat cores (#1957)Andres Noetzli
2018-03-21Refactor mkoptions (#1631)Mathias Preiner
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2017-08-04Set default language to smt lib 2.6 (including as a base language for sygus),...ajreynol
2017-06-28Enable non-linear solve by default, update regressions.ajreynol
2017-06-21Properly handle subtypes in smt2 printer.ajreynol
2017-06-02Fix regression.ajreynol
2017-06-02Incorporate datatypes into smt comp script, add regression.ajreynol
2017-04-05Fix several spelling errorsFabian Wolff
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback