summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
2018-08-16Refactor extended rewriter preprocessing pass (#2324)Haniel Barbosa
2018-08-16Refactor apply2const (#2316)Haniel Barbosa
2018-08-15Make sort inference a preprocessing pass (#2309)Andrew Reynolds
2018-08-13Fix get-unsat-assumptions output (#2301)Andres Noetzli
2018-08-07Fix inference of pre and post conditions for non variable arguments. (#2237)Andrew Reynolds
2018-08-02Parse standard separation logic inputs (#2257)Andrew Reynolds
2018-07-30Add support for incremental eager bit-blasting. (#1838)Mathias Preiner
2018-07-26Disabling bvLazyRewriteExtf in the right place (#2214)yoni206
2018-07-23 sygusComp2018: add regressions (#2191)Andrew Reynolds
2018-07-17Refactor sep-pre-skolem-emp preprocessing passyoni206
2018-07-13Properly clean up assertion stack in CnfProof (#2147)Andres Noetzli
2018-07-13 sygusComp2018: optimization for collect model info (#2105)Andrew Reynolds
2018-07-02Add regression test for issue #1986 (#2114)Andres Noetzli
2018-06-12Fix strip constant endpoint for ITOS in strings rewriter (#2067)Andrew Reynolds
2018-06-08Reset decisions at SAT level after solving (#2059)Andres Noetzli
2018-06-04Only enable transcendentals if logic is N[I]RAT (#2052)Andres Noetzli
2018-06-04Regressions: Support for requiring CVC4 features (#2044)Andres Noetzli
2018-06-02Fix BV-abstraction check to consider SKOLEM. (#2042)Mathias Preiner
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-30Fix bv-abstraction check for AND with non bit-vector atoms. (#2024)Mathias Preiner
2018-05-29 Make user's SMT2 version override file version (#2004)Andres Noetzli
2018-05-25Reenable repair const (#1983)Andrew Reynolds
2018-05-22Set same options for proofs as for unsat cores (#1957)Andres Noetzli
2018-05-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
2018-05-21Improvements in parsing and printing related to mixed int/real (#1879)Andrew Reynolds
2018-05-21Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)makaimann
2018-05-21Fix file extension (#1919)Caleb Donovick
2018-05-18Cegis unif defaults to cegis when no unif (#1942)Andrew Reynolds
2018-05-08Support for str.<= and str.< (#1882)Andrew Reynolds
2018-05-03Refactor bv-intro-pow2 preprocessing pass. (#1851)Mathias Preiner
2018-05-03Sets subtypes (#1095)Andrew Reynolds
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-04-25Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)yoni206
2018-04-25Fix issue with multi-triggers that include variable triggers (#1810)Andrew Reynolds
2018-04-20Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enab...yoni206
2018-04-12Fix alpha equivalence for higher-order (#1769)Andrew Reynolds
2018-04-10Properly implement function extensionality based on cardinality (#1765)Andrew Reynolds
2018-04-05 Python regression script (#1662)Andres Noetzli
2018-04-04Fix for corner case of higher-order matching (#1708)Andrew Reynolds
2018-03-23Add a few quantifiers regressions to improve coverage (#1702)Andrew Reynolds
2018-03-21Refactor mkoptions (#1631)Mathias Preiner
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
2018-03-21Fix various regression tests (#1657)Andres Noetzli
2018-03-20Fix datatype dump regression. (#1672)Andrew Reynolds
2018-03-19Enable CEGQI for non-linear (#1674)Andrew Reynolds
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-05Update semantics for string indexof and replace (#1630)Andrew Reynolds
2018-03-05Add support for check-sat-assuming. (#1637)Aina Niemetz
2018-02-27Improve rewriter for string indexof (#1592)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback