summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith
AgeCommit message (Expand)Author
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
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge com...Tim King
2017-01-10Adding regression test scrubbing.Tim King
2016-11-17Fix Makefiles in testAndres Notzli
2015-04-23Added option for --check-unsat-cores and various core bug fixes (merge of Mor...Liana Hadarean
2014-06-06Patch for the subtype theoryof mode to make the equalities over disequal type...Tim King
2014-03-05Improving support for POW in arithmetic. Resolves bug 549.Tim King
2014-02-19Merge branch '1.3.x'Tim King
2014-02-19Stopping non-linear terms from entering the dio solver. Fixes bug 547.Tim King
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof g...Morgan Deters
2013-12-09mv prp to regress1Kshitij Bansal
2013-12-07fix bug 542Kshitij Bansal
2013-12-04Remove a regression for which the portfolio takes forever (see bug 542).Morgan Deters
2013-11-25Substantial Changes:Tim King
2013-11-11Change exit status to be more consistent with other command-line tools: 0 suc...Morgan Deters
2013-09-18Support a personal build configuration and make rules.Morgan Deters
2013-09-13Move some regress benchmarks around that took too long, other test cleanup.Morgan Deters
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-05-09Changing the integer normal form to increase matching.Tim King
2013-04-26FCSimplex branch mergeTim King
2013-03-19Fixes for miplib-trick application (and a new testcase)Morgan Deters
2013-02-05Fix to miplib trick to make it less "cautious" and apply in more casesMorgan Deters
2013-02-03Some cleanup of miplib regressions and optionsMorgan Deters
2013-02-03new miplib pass, works for 1 or 2 varsMorgan Deters
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback