summaryrefslogtreecommitdiff
path: root/test/regress/regress0/Makefile.am
AgeCommit message (Expand)Author
2013-09-11Theory of strings.Tianyi Liang
2013-07-19enable bug521 regression testsMorgan Deters
2013-07-17Fix bug 516; include some bug testcases.Morgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
2013-07-09Fix for bug 519; don't involve ITESimplifier in model generation.Morgan Deters
2013-06-04Merge branch '1.2.x'Morgan Deters
2013-06-04Fix clang static initialization order issue; fixes bug 512.Morgan Deters
2013-05-22Add regressions for finite model findingAndrew Reynolds
2013-05-21Fix bug 512: an assertion failure only appearing with clang on Mac OS, due to...Morgan Deters
2013-05-21Fix incremental bug in symmetry breaker.Morgan Deters
2013-05-20Fix for equality-chaining of Booleans in SMT-LIBv2.Morgan Deters
2013-05-01Fix to boolean-terms; resolves bug #507Morgan Deters
2013-04-01Fix for iff terms over equalities between the same term and differing constants.Tim King
2013-04-01Fix bug 491 and related issues with checkModel() and quantifiers. Enabling p...Morgan Deters
2013-03-20Fix to bug 497: make justification heuristic's ITE cache context-dependent.Morgan Deters
2013-03-20Properly |quote| symbols in SMT-LIBv2 output.Morgan Deters
2013-02-07Merge branch '1.0.x'Morgan Deters
2013-02-07Significant work on bug #491 (not yet closed).Morgan Deters
2013-02-07More complete fix for bug 484 (includes fixes for records and tuples).Morgan Deters
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed b...Andrew Reynolds
2013-01-29currently disabling bug486 regression. we need to discuss getValue/collectMo...Andrew Reynolds
2013-01-28Fix the regression test for bug 486, and enable itMorgan Deters
2013-01-28Fix the regression test for bug 486, and enable itMorgan Deters
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2012-12-11SMT-LIB compliance fix to get-assignment; resolves bug 480Morgan Deters
2012-12-01Some fixes for boolean arraysMorgan Deters
2012-11-27Functions and predicates over Boolean now work with --check-models and output...Morgan Deters
2012-11-27First chunk of boolean-terms support.Morgan Deters
2012-11-14Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ...Tim King
2012-10-22add bug 425 models regression; fix mac-build execute permissionMorgan Deters
2012-10-11Fix bug 421, again, and add a second, independent test case for the sameMorgan Deters
2012-10-10Abstract values for SMT-LIB.Morgan Deters
2012-10-06* Include a few bug testcases for resolved bugs.Morgan Deters
2012-09-26bug #398 test (bug was resolved last night), and a script to download all bug...Morgan Deters
2012-09-21SMT-LIBv2 compliance updates:Morgan Deters
2012-09-16enable bug regression for bug 382Morgan Deters
2012-09-15bug testcase for model generationMorgan Deters
2012-09-06Remove SmtEngine::getStackLevel(), which exposed implementation details and w...Morgan Deters
2012-08-28fix regression tests for automake 1.11 and automake 1.12---both versions shou...Morgan Deters
2012-08-21add some incremental in-tree regressionsMorgan Deters
2012-07-27Merge quantifiers2-trunk:François Bobot
2012-07-08Bugs resolved by this commit: #314, #322, #359, #364, #365.Morgan Deters
2012-06-22TPTP: add parser for cnf and fofFrançois Bobot
2012-06-14don't run rewriterules regressions by default; fixes neededMorgan Deters
2012-06-13removing bug233 until morgan commits the actual fileDejan Jovanović
2012-06-13adding some regressions to the usual regressions runs; several recently-fixed...Morgan Deters
2012-06-13decision regressions, all but one failKshitij Bansal
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback