summaryrefslogtreecommitdiff
path: root/test/unit
AgeCommit message (Expand)Author
2014-07-01Update copyrights.Morgan Deters
2014-06-25BinaryHeap unit test and some usability/build fixes for the data structure it...Morgan Deters
2014-06-21Some minor cleanup and documentation.Morgan Deters
2014-06-21fixed build failurelianah
2014-06-19added model generation to eager bit-blasting and turned abc off by defaultlianah
2014-06-19disable unate lemmas when using incremental modeKshitij Bansal
2014-06-11Merge pull request #31 from kbansal/setsKshitij Bansal
2014-06-11fixed unit tests failureslianah
2014-06-11disable failing testKshitij Bansal
2014-05-27update stats_blackKshitij Bansal
2014-04-01Merge branch '1.3.x'Tim King
2014-04-01Fixing bug 552. There was a bug when integers are made using a string with a...1.3.xTim King
2014-03-12Fix LogicInfo unit test.Morgan Deters
2014-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r...Morgan Deters
2014-02-21add new theory (sets)Kshitij Bansal
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after final...Morgan Deters
2013-12-24Better automatic handling of output language setting.Morgan Deters
2013-12-10Fix timer statistics to report correct time even on process abort.Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-02Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a s...Morgan Deters
2013-11-20Changing the number of bits allocated per field in node values.Tim King
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-09-11Theory of strings.Tianyi Liang
2013-09-09Add support for check-sat with argument.Morgan Deters
2013-06-27Remove output.h from public space, to avoid clashes with symbols defined in u...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-29Merge branch '1.2.x'Morgan Deters
2013-05-28Standardize SMT-LIBv2 set of logics to use LogicInfo.Morgan Deters
2013-05-09Changing the integer normal form to increase matching.Tim King
2013-05-03Fixing compilation of unit tests. These problems were due to splitLemma() bei...Tim King
2013-04-05Fix unit test (compile error) for new SatSolver interfaceMorgan Deters
2013-04-03Some final minor changes before cutting 1.1.Morgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-21Some model and printing fixes for defined functions in input.Morgan Deters
2013-03-20Interactive mode support for multiline inputMorgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds an...Morgan Deters
2013-02-04Fix NodeBuilder bug which could attempt to allocate beyond hard limitMorgan Deters
2012-12-14Adding unit test for different versions of division.Tim King
2012-12-08Fix bug 476: when CxxTest is not found, make the error less fatal-lookingMorgan Deters
2012-11-30Fixes for stricter compilers Andy brought to my attention.Tim King
2012-11-30Committing tests to potentially discover an obscure CLN library issue on 32 b...Tim King
2012-11-26Improved implementation of Integer::length() with CLN enabled. Additional te...Tim King
2012-11-17* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT...Morgan Deters
2012-11-10Updates to Clark's commit r4540:Morgan Deters
2012-11-08Review of trunk r4525 (TypeNode::getBaseType()):Morgan Deters
2012-10-26Fix to subrange type enumerator, and its unit test. Resolves bug 436.Morgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-06* Fix some regressions' expected outputs.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback