summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2011-07-11if running in QF_AX, equalities over terms of uninterpreted sort go to arrays...Morgan Deters
2011-07-11minimized exampleMorgan Deters
2011-07-11array benchmarksMorgan Deters
2011-07-11merge from symmetry branchMorgan Deters
2011-07-09minor fixupsMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
2011-07-05missing test caseDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30only use theory registration if (1) a theory requests it, or (2) if there's m...Morgan Deters
2011-06-30some things I had laying around in a directory but never got committed; minor...Morgan Deters
2011-06-02minor fix to build system for system testsMorgan Deters
2011-06-02added (temporary) support for ensuring that all ambiguously typed constructor...Andrew Reynolds
2011-05-31This commit contains the code for allowing arbitrary equalities in the theory...Tim King
2011-05-23fixes for "make dist" and "make doc", minor cleanupsMorgan Deters
2011-05-23Merge from arrays2 branch.Morgan Deters
2011-05-13* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolioMorgan Deters
2011-05-06added 10 benchmarks to regress/regress0/datatypes from paperAndrew Reynolds
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
2011-05-04Stronger support for zero-performance-penalty output, and fixes andMorgan Deters
2011-05-02adding some previously-failing "bug" test cases for bitvectorsMorgan Deters
2011-05-02updating bv regressionsDejan Jovanović
2011-05-02more minor fixes related to last few commitsMorgan Deters
2011-05-02fix broken build; sorry, all!Morgan Deters
2011-05-01minor fixes, plus experimental readline support in InteractiveShellMorgan Deters
2011-04-25Monday tasks:Morgan Deters
2011-04-25small unit test fix; was broken only in non-assertion, non-CLN buildsMorgan Deters
2011-04-25Weekend work. The main points: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-23make run_regression script robust to DOS newlines :(Morgan Deters
2011-04-20numerous bugfixesMorgan Deters
2011-04-20incorrect usage of C++ std::string caused a test to failMorgan Deters
2011-04-20Minor mixed-bag commit. Expected performance impact negligible.Morgan Deters
2011-04-20Tuesday end-of-day commit.Morgan Deters
2011-04-18more work on CVC languageMorgan Deters
2011-04-18mostly CVC presentation language parsing and printingMorgan Deters
2011-04-18This commit merges the branch arithmetic/propagation-again into trunk.Tim King
2011-04-18Partial merge from datatypes-merge branch:Morgan Deters
2011-04-16also a fix for a system test related to ParserBuilderMorgan Deters
2011-04-16unit test fixes for new NodeManager constructor (related to previous two trun...Morgan Deters
2011-04-11Transitive closure module is workingClark Barrett
2011-04-11fix "make dist" issues in makefilesMorgan Deters
2011-04-08Added util classClark Barrett
2011-04-05Minor adjustments to the Registrar commit in 1644, documentation.Morgan Deters
2011-04-04Merging the satliteral-before-prereg branch into trunk. Theory preregistratio...Tim King
2011-04-04Reverts previous commit r1636.Tim King
2011-04-04Add documentation to Node and TNode (closes bug #201).Morgan Deters
2011-04-02Delayed the addition of unate propagation lemmas until propagation is called....Tim King
2011-04-01This commit is a merge from the "betterstats" branch, which:Morgan Deters
2011-03-30improve recent low-coverage complaintsMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback