summaryrefslogtreecommitdiff
path: root/test/regress/Makefile.tests
AgeCommit message (Expand)Author
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
2018-04-06Add define rec fun to cvc parser (#1738)Arjun Viswanathan
2018-04-04Fix for corner case of higher-order matching (#1708)Andrew Reynolds
2018-04-03Option to turn arbitrary input into sygus (#1704)Andrew Reynolds
2018-04-03Use choice when expanding definitions for inverse transcendental functions (#...Andrew Reynolds
2018-03-30Disable regression (#1731)Andrew Reynolds
2018-03-23Add a few quantifiers regressions to improve coverage (#1702)Andrew Reynolds
2018-03-21 Move regression tests to single Makefile.am (#1658)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback