summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Expand)Author
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-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-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-05 Python regression script (#1662)Andres Noetzli
2018-04-04Update README for regression tests (#1746)Andres Noetzli
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-04-02Remove references to nyu (#1721)Clark Barrett
2018-03-30Disable regression (#1731)Andrew Reynolds
2018-03-26Add support for filtering regressions with regex (#1711)Andres Noetzli
2018-03-23Add a few quantifiers regressions to improve coverage (#1702)Andrew Reynolds
2018-03-21Fix 'make regress' (#1683)Andres Noetzli
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-21Fix for string disequality processing (#1679)Andrew Reynolds
2018-03-20Internally remove redundant assertions and infer equalities in NonLinearExten...Andrew Reynolds
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-09Skip (get-unsat-assumptions) tests not supported (#1656)Andres Noetzli
2018-03-08Fix Travis for unit test compilation errors. (#1651)Mathias Preiner
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-27Minor fixes for rec-fun (#1616)Andrew Reynolds
2018-02-27Improve rewriter for string indexof (#1592)Andrew Reynolds
2018-02-23Fix cd-simplification for strings (#1624)Andrew Reynolds
2018-02-22Minor improvements to string rewriter (#1572)Andrew Reynolds
2018-02-20Minor fixes and additions for transcendental functions (#1612)Andrew Reynolds
2018-02-16Make regress1 default, only test regress0 on Travis. (#1611)Aina Niemetz
2018-02-15Fix corner case for rewrite of mult by pow 2 (#1601)Andrew Reynolds
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2018-02-08Remove invalid regression test (#1579)Andres Noetzli
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback