Age | Commit message (Expand) | Author |
2012-09-21 | SMT-LIBv2 compliance updates: | Morgan Deters |
2012-09-21 | better verbosity support (so it's sensible when the library is used via the API) | Morgan Deters |
2012-09-19 | General subscriber infrastructure for NodeManager, as discussed in the | Morgan Deters |
2012-09-18 | SMT-LIBv2 compliance regarding outputting "unknown". | Morgan Deters |
2012-09-17 | minor fix for models, added simple cliques option for uf strong solver | Andrew Reynolds |
2012-09-16 | enable bug regression for bug 382 | Morgan Deters |
2012-09-15 | bug testcase for model generation | Morgan Deters |
2012-09-06 | Remove SmtEngine::getStackLevel(), which exposed implementation details and w... | Morgan Deters |
2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
2012-08-29 | To the build system: | Morgan Deters |
2012-08-28 | test summaries for automake 1.12 test harness | Morgan Deters |
2012-08-28 | fix regression tests for automake 1.11 and automake 1.12---both versions shou... | Morgan Deters |
2012-08-28 | Improved compatibility layer, now supports quantifiers. Also incorporates | Morgan Deters |
2012-08-27 | * Reversing commit r4258 (which disabled failing regressions). Fixed the pro... | Morgan Deters |
2012-08-26 | disabling failing regressions | Kshitij Bansal |
2012-08-26 | Array constants finished and working. Unit tests for array constants. | Clark Barrett |
2012-08-25 | fix unit tests | Morgan Deters |
2012-08-22 | Cap finite cardinalities at 2^64, as discussed in the meeting last week. | Morgan Deters |
2012-08-21 | add some incremental in-tree regressions | Morgan Deters |
2012-08-20 | removing v1l20009.cvc, a datatypes benchmark where the TCC fails (CVC3 and CV... | Morgan Deters |
2012-08-16 | The SmtEngine now ensures that setLogicInternal() is called even if there is ... | Morgan Deters |
2012-08-16 | bug 374 (was found through fuzzing 2012-07-18) | Kshitij Bansal |
2012-08-16 | ArrayStoreAll should (for now) only allow constant expressions, as it is itse... | Morgan Deters |
2012-08-14 | Fixes to integer wrapper classes: | Morgan Deters |
2012-08-07 | Some items from the CVC4 public interface review: | Morgan Deters |
2012-08-05 | Disable failing datatypes regression, pending solution to bug #370. | Morgan Deters |
2012-08-04 | isConst() rule for datatypes | Morgan Deters |
2012-08-03 | Comparisons for LogicInfos, and associated tests | Morgan Deters |
2012-08-03 | ArrayStoreAll infrastructure | Morgan Deters |
2012-08-01 | fixes to some *clean targets | Morgan Deters |
2012-07-31 | Options merge. This commit: | Morgan Deters |
2012-07-27 | Minor cleanup after today's commits: | Morgan Deters |
2012-07-27 | removing unecessary files | Andrew Reynolds |
2012-07-27 | merging fmf-devel branch, includes refactored datatype theory, updates to mod... | Andrew Reynolds |
2012-07-27 | Merge quantifiers2-trunk: | François Bobot |
2012-07-26 | Datatype enumerator work. This version is not a "fair" enumerator, but I got... | Morgan Deters |
2012-07-18 | a few fixes for java system test | Morgan Deters |
2012-07-16 | now passes "make distcheck", which does important checks for the release (e.g... | Morgan Deters |
2012-07-16 | fix compiler warning in unit test | Morgan Deters |
2012-07-16 | stronger two_smt_engines test | Morgan Deters |
2012-07-16 | fix inadvertent change to system test | Morgan Deters |
2012-07-16 | Support for having two SmtEngines with the same ExprManager. | Morgan Deters |
2012-07-14 | Type enumerator infrastructure and uninterpreted constant support. No suppor... | Morgan Deters |
2012-07-14 | fix a warning in unit test compilation | Morgan Deters |
2012-07-08 | Bugs resolved by this commit: #314, #322, #359, #364, #365. | Morgan Deters |
2012-07-07 | Various fixes to documentation---typos, some incomplete documentation fixed, ... | Morgan Deters |
2012-06-28 | Fixed bug in bv rewriter that caused wrong answer in SMT-COMPsmtcomp2012-resubmission-2 | Clark Barrett |
2012-06-22 | TPTP: add parser for cnf and fof | François Bobot |
2012-06-17 | enabling theoryof=term for quantifiers with sharing | Dejan Jovanović |
2012-06-17 | fixing wrong assertion | Dejan Jovanović |