summaryrefslogtreecommitdiff
path: root/test/regress/Makefile.tests
AgeCommit message (Expand)Author
2018-06-13Fix simple regexp consume (#2066)Andrew Reynolds
2018-06-12Fix strip constant endpoint for ITOS in strings rewriter (#2067)Andrew Reynolds
2018-06-10Fix equality conflicts reported by FP (#2064)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-04Enable cegqi (with model values) for floating point by default (#2023)Andrew Reynolds
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-02Fix preinitialization pass for finite model finding (#2047)Andrew Reynolds
2018-06-01Fix quantified bv variable elimination (#2039)Andrew Reynolds
2018-06-01Apply preprocessing to counterexample lemmas in CEGQI (#2027)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-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)Andrew Reynolds
2018-05-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
2018-05-22Make sygus infer find function definitions (#1951)Andrew Reynolds
2018-05-21Infrastructure to mark unused sygus strategies (#1950)Andrew Reynolds
2018-05-21Fix file extension (#1919)Caleb Donovick
2018-05-18Unified fairness scheme for cegis unif (#1941)Andrew Reynolds
2018-05-17Fix debugPrint and add regress. (#1934)Andrew Reynolds
2018-05-17Cegis-specific infrastructure (#1933)Andrew Reynolds
2018-05-15adding regressions (#1925)Haniel Barbosa
2018-05-14Add regressions, change defaults. (#1911)Andrew Reynolds
2018-05-14Flag to check invariance of entire values in sygus explain (#1908)Andrew Reynolds
2018-05-11Remove obsolete unit test for ackermannization. (#1906)Aina Niemetz
2018-05-11Fix ackermannize preprocessing pass. (#1904)Aina Niemetz
2018-05-10Sygus repair constants (#1812)Andrew Reynolds
2018-05-09Make symmetry-breaker-exp into a preprocessing pass (#1890)Andrew Reynolds
2018-05-08Refactor bv-abstraction preprocessing pass. (#1860)Mathias Preiner
2018-05-08Support for str.<= and str.< (#1882)Andrew Reynolds
2018-05-07Add support for str.code (#1821)Andrew Reynolds
2018-05-03Refactor bv-intro-pow2 preprocessing pass. (#1851)Mathias Preiner
2018-05-03Sets subtypes (#1095)Andrew Reynolds
2018-05-03Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)Andrew Reynolds
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-04-30Refactor real2int (#1813)Haniel Barbosa
2018-04-29Allow multiple functions in sygus unif approaches (#1831)Andrew Reynolds
2018-04-29Make factoring inference more aggressive (#1825)Andrew Reynolds
2018-04-25Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)yoni206
2018-04-25Add benchmark requiring subgoal generation with induction. Disable option. (#...Andrew Reynolds
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-20Symmetry detection module (#1749)PaulMeng
2018-04-19Refactor pbRewrites preprocessing pass (#1767)Andres Noetzli
2018-04-16Disable slow regression test (#1787)Andres Noetzli
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-09Fix hasSubterm calls for higher-order (#1760)Andrew Reynolds
2018-04-09Fix higher-order term indexing. (#1754)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback