summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Expand)Author
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
2018-02-06Fix two multiply-by-constant corner cases for bv rewriter (#1562)Andrew Reynolds
2018-02-06Fix rewrite for string replace (#1537)Andrew Reynolds
2018-02-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
2018-02-02Fix remaining synthesis solution regressions (#1557)Andrew Reynolds
2018-02-02Option to check solutions produced by SyGuS solver (#1553)Haniel Barbosa
2018-01-21Refactor and fix solveBvLit for CBQI BV. (#1526)Aina Niemetz
2018-01-12Improvements for CBQI BV (#1504)Andrew Reynolds
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
2018-01-03Global negate (#1466)Andrew Reynolds
2018-01-02Rewrites for BitVector multiplication (#1465)Andrew Reynolds
2017-12-27Rel smt parser (#1446)Arjun Viswanathan
2017-12-20Fixes for cbqi-bv (#1449)Andrew Reynolds
2017-12-20Add explicit disequality handling when generating side condition for CBQI BV....Aina Niemetz
2017-12-20Transcendental functions check model (#1443)Andrew Reynolds
2017-12-10Fix issue 1433. (#1435)Andrew Reynolds
2017-12-08Fixed side conditions for CBQI BV, added unit tests. (#1434)Aina Niemetz
2017-12-07Fixes related to SyGuS + real arithmetic (#1432)Andrew Reynolds
2017-12-06Remove CDChunkList (#1414)Andres Noetzli
2017-12-04Fix strings rewriter for strip constant endpoint reverse direction (#1424)Andrew Reynolds
2017-12-01Fix reset-assertions (#1413)Andres Noetzli
2017-12-01Refactor and generalize PBE strategies (#1410)Andrew Reynolds
2017-11-29Improve caching in term formula removal (#1398)Andrew Reynolds
2017-11-28Improve rewrite for string substr (#1337)Andrew Reynolds
2017-11-27Fix models for --solve-real-as-int. (#1371)Andrew Reynolds
2017-11-25Fixes for higher-order (#1405)Andrew Reynolds
2017-11-24Implement tangent and secant planes for transcendental functions (#1401)Andrew Reynolds
2017-11-23Ho parsing and regressions (#1350)Andrew Reynolds
2017-11-21Cegqi bv remove extract terms preprocess pass (#1376)Andrew Reynolds
2017-11-15Reenable some regressions, minor. (#1369)Andrew Reynolds
2017-11-14Clean Ceg Instantiators (#1365)Andrew Reynolds
2017-11-13Disable sygus qe preprocessing by default (#1353)Andrew Reynolds
2017-11-13Argument Relevance for Synthesis Conjectures (#1311)Andrew Reynolds
2017-11-05Improve rewriting for string contains part 2 (#1300)Andrew Reynolds
2017-11-03Suppport SAT logic (#1310)Andrew Reynolds
2017-11-03Sygus clean main (#1297)Andrew Reynolds
2017-11-01CBQI BV choice expressions (#1296)Andrew Reynolds
2017-10-28Change bvudiv semantics based on input language (#1292)Andres Noetzli
2017-10-27Improve strings rewriter for contains (#1207)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback