summaryrefslogtreecommitdiff
path: root/test/regress/regress0/Makefile.am
AgeCommit message (Expand)Author
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
2012-06-06unconstrained regressions are now run with "make check", but with --unconstra...Morgan Deters
2012-06-06Fixing numerous issues with tests and "make dist":Morgan Deters
2012-05-18This commit adds TypeNode::leastCommonTypeNode(). The special case for arith...Tim King
2012-05-18removing failing regressionDejan Jovanović
2012-05-17Adding failing regression for ite type computation.Tim King
2012-05-15test casesDejan Jovanović
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-05Support to test the "dumper" mechanism in regressions (feeding dump output ba...Morgan Deters
2012-03-22some improvements to the sharing mechanism/interfaceDejan Jovanović
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2012-02-29fixing bug310Dejan Jovanović
2012-02-21Fix for bug303. The problem was with function applications that get normalize...Dejan Jovanović
2012-02-20portfolio mergeMorgan Deters
2012-02-15This commit merges into trunk the branch branches/arithmetic/integers2 from r...Tim King
2011-11-30disable bug288.smt so that "make check" goes through---pending integers merge...Morgan Deters
2011-11-30Adding a failing UFLIA benchmark corresponding to bug #288.Tim King
2011-10-29Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::g...Morgan Deters
2011-10-28proof regressionsMorgan Deters
2011-09-30fixes to incremental simplification, cnf routines, other stuff in preparation...Morgan Deters
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-05-23Merge from arrays2 branch.Morgan Deters
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
2011-04-23fix for parser/tests for ANTLR 3.2 (it was working fine on 3.3)Morgan Deters
2011-04-23* reviewed BooleanSimplification, added documentation & unit testMorgan Deters
2011-04-18Partial merge from datatypes-merge branch:Morgan Deters
2011-03-30improve recent low-coverage complaintsMorgan Deters
2011-03-30Add Valuation::getSatValue() so that theories can access the currentMorgan Deters
2011-03-26fix typoMorgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2011-03-10ITE removal in TheoryEngine was not properly handling PARAMETERIZED kinds. F...Morgan Deters
2011-03-05adding three features to CVC parser that drastically improve its support for ...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback