summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2018-05-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)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-22Make sygus infer find function definitions (#1951)Andrew Reynolds
2018-05-21Improvements in parsing and printing related to mixed int/real (#1879)Andrew Reynolds
2018-05-21Infrastructure to mark unused sygus strategies (#1950)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-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-14Fix annotations in regress2. (#1917)Andrew Reynolds
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-10Support multiple sets of command line args in regs (#1902)Andres Noetzli
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-05-01Improve tangent planes for transcendental functions (#1832)Andrew Reynolds
2018-04-30Refactor real2int (#1813)Haniel Barbosa
2018-04-30Disable unsat-cores/proofs for slow regression (#1835)Andres Noetzli
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-20Allow metadata lines in test files to have leading spaces (#1799)yoni206
2018-04-20Symmetry detection module (#1749)PaulMeng
2018-04-20Restrict test summary to first-level subfolders (#1797)Andres Noetzli
2018-04-19Refactor pbRewrites preprocessing pass (#1767)Andres Noetzli
2018-04-16Add timeout (option) to regression script (#1786)Andres Noetzli
2018-04-16Disable slow regression test (#1787)Andres Noetzli
2018-04-16Disable check proofs/unsat cores for two regs (#1785)Andres Noetzli
2018-04-14[Reg] Make status/unsat-core detection more robust (#1775)Andres Noetzli
2018-04-14Fix get-unsat-core detection in regression script (#1773)Andres Noetzli
2018-04-13Fix issue in regression script when proofs enabled (#1770)Andres Noetzli
2018-04-12Fix alpha equivalence for higher-order (#1769)Andrew Reynolds
2018-04-10Refactored BVGauss preprocessing pass. (#1766)Aina Niemetz
2018-04-10Properly implement function extensionality based on cardinality (#1765)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback