summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2010-02-22resolve bug 32; public-facing interface functions in expr package must set cu...Morgan Deters
2010-02-22fix bug 22 (remove tracing from non-trace builds; remove all outputMorgan Deters
2010-02-19specialized implementation for boolean node attributes ("flags"): they now sh...Morgan Deters
2010-02-19* Attribute infrastructure -- static design. Documentation is coming.Morgan Deters
2010-02-16Converting semantic predicates in parser to AlwaysAssertionsChristopher L. Conway
2010-02-11Adding precedence regressionsChristopher L. Conway
2010-02-09Changes to the CNF conversion and the SAT solver. All regression pass now, an...Dejan Jovanović
2010-02-08Disabling the failing test case for the context.Dejan Jovanović
2010-02-08Fixing the test case, it had a unary or. The cnf converter should be adapted ...Dejan Jovanović
2010-02-06Preliminary support for types in parserChristopher L. Conway
2010-02-04fix run_regression scriptMorgan Deters
2010-02-04assign expected-status to regressionsMorgan Deters
2010-02-04build system for multi-level regressionsMorgan Deters
2010-02-04remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing...Morgan Deters
2010-02-04Moved regressions into various levels based on running time.Tim King
2010-02-04test infrastructure updated for multiple-level regressionsMorgan Deters
2010-02-04src/expr/kind.h is now automatically generated.Morgan Deters
2010-02-04minor fix for update-copyright.pl; ran update-copyright.pl on all sources; re...Morgan Deters
2010-02-03Adding extra test to parserChristopher L. Conway
2010-02-03Adding functions/predicates to SMT grammarChristopher L. Conway
2010-02-03simple ITE parsingDejan Jovanović
2010-02-03Enabled more regress tests. Takes 26s on my machine to run a make -k check in...Tim King
2010-02-03context_mm testingDejan Jovanović
2010-02-03some more tests for the context.Dejan Jovanović
2010-02-02beginings of test for CDO. one failDejan Jovanović
2010-02-02Minor changes to parserChristopher L. Conway
2010-02-01Fixing the CVC grammar for parsing Boolean expressions. All the associativity...Dejan Jovanović
2010-02-01Added this test back to avoid make check problems.Tim King
2010-01-30Checking in small test fixes for node_blackTim King
2010-01-29fixed CNF conversion, and more modular; CNF conversion command line option; v...Morgan Deters
2010-01-28Removing Makefile.in'sChristopher L. Conway
2010-01-27support "make check" in src/ subdirs for unit-testing of just that module; al...Morgan Deters
2010-01-27test framework fixes; bug 13 closedMorgan Deters
2010-01-27Added additional tests to node_black.h. CVC4 currently passes all but 1 test.Tim King
2010-01-26Undoing stupid commit mistake. Rolling back to -r 102 for test/unit/expr/nod...Tim King
2010-01-26Added test/regress/boolean.cvcTim King
2010-01-26fixes to build structure, util classes, lots of fixes to Node and NodeBuilder...Morgan Deters
2010-01-23Added pure PL regression tests. Mostly CNFTim King
2010-01-22Added regression testTim King
2009-12-18More fixes fot the parser tests.Dejan Jovanović
2009-12-18Changing some deatils on the parser. Now we know we are done if command is nu...Dejan Jovanović
2009-12-18Updated parser tests, which are all kinds of FAILChristopher L. Conway
2009-12-18Changes to the parser tests to make them compile.Dejan Jovanović
2009-12-17more build system fix-upsMorgan Deters
2009-12-17update-copyright.pl now retrieves and incorporates author information from re...Morgan Deters
2009-12-17Adding more parser testsChristopher L. Conway
2009-12-17Adding more parser testsChristopher L. Conway
2009-12-17CvcParserBlack and supporting Makefile changesChristopher L. Conway
2009-12-17+ test infrastructure fixesMorgan Deters
2009-12-17add system regression testing infrastructureMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback