summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
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
2011-03-30Add Valuation::getSatValue() so that theories can access the currentMorgan Deters
2011-03-26fix for bug 253, was propagating an asserted literalDejan Jovanović
2011-03-26fix typoMorgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2011-03-25Fix for a bug Andrew Reynolds found for iterators that affects empty CDList<>...Morgan Deters
2011-03-21more bugfixes, some basic propagation, and testcases to cover themDejan Jovanović
2011-03-21fixing a bug in the BV rewrite, off by one error when merging constantsDejan Jovanović
2011-03-20more bugfixes for bitvectorsDejan Jovanović
2011-03-20missed one caseDejan Jovanović
2011-03-20commit for the version of bitvectors that passes all the unit testsDejan Jovanović
2011-03-15small fixes for run_regression script to workaround bug in old mktemp, was ca...Morgan Deters
2011-03-15Merge from cudd branch. This mostly just adds support for linkingMorgan Deters
2011-03-14change to the run_regression script to better manage temporary files; hopeful...Morgan Deters
2011-03-10Fix bug 246 (occasional buffer overflow related to varargs in assertion-failu...Morgan 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
2011-02-28Review of statistics code. Added lots of documentation, and fixed an issue (...Morgan Deters
2011-02-26Merge from theory-break-dependences branch to break Theory and TheoryEngine d...Morgan Deters
2011-02-17some unit tests to work on slicingDejan Jovanović
2011-01-05fix for build errorsDejan Jovanović
2011-01-05Commit for the theory engine and rewriter changes. Changes are substantial an...Dejan Jovanović
2010-12-14congruence closure module now supports things other than APPLY_UF; ported fro...Morgan Deters
2010-12-14fix to static learning application in UF, resolves bug# 239Morgan Deters
2010-11-19Merge from ufprop branch, including:Morgan Deters
2010-11-17fix improper CongruenceClosureWhite test by merging from a uf branch; fixes t...Morgan Deters
2010-11-16Added Theory::presolve().Tim King
2010-11-16SmtEngine now fails with a ModalException if --incremental is not enabledMorgan Deters
2010-11-15Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printerMorgan Deters
2010-11-15This commit merges the arith-prop-opt branch into the main trunk. This was do...Tim King
2010-11-15minor tweaks to last commit, testing infrastructureMorgan Deters
2010-11-15fix some things with the build system (make dist, make install, make check)Morgan Deters
2010-11-09Lemmas on demand work, push-pop, some cleanup.Dejan Jovanović
2010-10-29Adds a very small test that triggers a bug. The bug is from the commit for -r...Tim King
2010-10-27fix test MakefileMorgan Deters
2010-10-26Cleaning up some header filesChristopher L. Conway
2010-10-24Adding unit test for InteractiveShellChristopher L. Conway
2010-10-22Merging main/getopt.cpp, main/usage.h, and smt/options.h inChristopher L. Conway
2010-10-21* Option --no-type-checking now disables type checks in SmtEngineChristopher L. Conway
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback