summaryrefslogtreecommitdiff
path: root/test/unit
AgeCommit message (Expand)Author
2013-11-07Flatten 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
2012-10-05Bug-related:Morgan Deters
2012-10-03adding ::getBooleanVariables to the PropEngineDejan Jovanović
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-09-28Public interface review items:Morgan Deters
2012-09-27* Rename SMT parts (printer, parser) to SMT1Morgan Deters
2012-09-24some api changesDejan Jovanović
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-09-21better verbosity support (so it's sensible when the library is used via the API)Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-29To the build system:Morgan Deters
2012-08-26Array constants finished and working. Unit tests for array constants.Clark Barrett
2012-08-25fix unit testsMorgan Deters
2012-08-22Cap finite cardinalities at 2^64, as discussed in the meeting last week.Morgan Deters
2012-08-16The SmtEngine now ensures that setLogicInternal() is called even if there is ...Morgan Deters
2012-08-16ArrayStoreAll should (for now) only allow constant expressions, as it is itse...Morgan Deters
2012-08-14Fixes to integer wrapper classes:Morgan Deters
2012-08-07Some items from the CVC4 public interface review:Morgan Deters
2012-08-04isConst() rule for datatypesMorgan Deters
2012-08-03Comparisons for LogicInfos, and associated testsMorgan Deters
2012-08-03ArrayStoreAll infrastructureMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback