Age | Commit message (Expand) | Author |
2012-10-10 | Abstract values for SMT-LIB. | Morgan Deters |
2012-10-10 | fixing the cvc bv parser and typechecker | Dejan Jovanović |
2012-10-09 | * make Model class private (as discussed at meeting today) | Morgan Deters |
2012-10-09 | made datatypes rewrite incorrect selectors to ground term. this feature can ... | Andrew Reynolds |
2012-10-09 | fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 4... | Morgan Deters |
2012-10-08 | * Models' SubstitutionMaps are now attached to the user context | Morgan Deters |
2012-10-08 | added reduced bv model failing test case | Liana Hadarean |
2012-10-06 | * Include a few bug testcases for resolved bugs. | Morgan Deters |
2012-10-06 | * Fix some regressions' expected outputs. | Morgan Deters |
2012-10-05 | Bug-related: | Morgan Deters |
2012-10-03 | adding ::getBooleanVariables to the PropEngine | Dejan Jovanović |
2012-09-28 | rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak... | Morgan Deters |
2012-09-28 | Public interface review items: | Morgan Deters |
2012-09-28 | * fix compatibility library naming for SMT-LIBv1 | Morgan Deters |
2012-09-27 | * Rename SMT parts (printer, parser) to SMT1 | Morgan Deters |
2012-09-26 | disable building of cvc3_george system-test object (which isn't used yet anyw... | Morgan Deters |
2012-09-26 | bug #398 test (bug was resolved last night), and a script to download all bug... | Morgan Deters |
2012-09-25 | some buggy examples for incrementality, and make bug326 run as part of make r... | Morgan Deters |
2012-09-24 | some api changes | Dejan Jovanović |
2012-09-22 | Separate public-facing and internal-facing interfaces to Statistics. | Morgan Deters |
2012-09-21 | Fixes for datatype dumping and printing. Add a new test case for dumping. | Morgan Deters |
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 |