| Age | Commit message (Expand) | Author |
|---|
| 2012-11-17 | * Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT... | Morgan Deters |
| 2012-11-16 | Fix for bug451 | Clark Barrett |
| 2012-11-15 | More fixes to model generation, with previously failing testcases | Clark Barrett |
| 2012-11-15 | fuzz15 should have been fuzz14 | Clark Barrett |
| 2012-11-15 | Fix for bug 447. | Tim King |
| 2012-11-15 | Fixed another AUFBV model bug. BV equality subtheory needed to do something | Clark Barrett |
| 2012-11-15 | Fixing comments in print_lambda.cvc. | Tim King |
| 2012-11-14 | Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ... | Tim King |
| 2012-11-14 | Fix to bug449. Adds shared constants to the set of DeltaRationals that must b... | Tim King |
| 2012-11-14 | bug fixes to models, array rewriter with previously failing testcases | Clark Barrett |
| 2012-11-13 | added support for division by zero for bit-vector division operators | Liana Hadarean |
| 2012-11-13 | Fixed an array rewriting bug found by fuzzer | Clark Barrett |
| 2012-11-13 | Testcases for fixed bugs | Clark Barrett |
| 2012-11-12 | Improved error reporting for improperly using non-linear division in linear a... | Tim King |
| 2012-11-12 | Delta is now generated in arithmetic to keep consistent the total order of De... | Tim King |
| 2012-11-10 | Fixed missing \ in uflra/Makefile.ma | Clark Barrett |
| 2012-11-10 | Fix for bug 439. Delta computation now includes disequality information. | Tim King |
| 2012-11-10 | Change run-regression script to *additionally* run a second test with --check... | Morgan Deters |
| 2012-11-10 | Updates to Clark's commit r4540: | Morgan Deters |
| 2012-11-09 | Test that breaks arithmetic model building due to disequality terms. | Tim King |
| 2012-11-09 | Arithmetic problem that fails --check-models due incompleteness with multipli... | Tim King |
| 2012-11-08 | Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases fo... | Tim King |
| 2012-11-08 | Review of trunk r4525 (TypeNode::getBaseType()): | Morgan Deters |
| 2012-11-07 | * Type ascription bug fixed (resolves bug 432), but there are others I discov... | Morgan Deters |
| 2012-11-07 | Fix to a bug in integer mod lemmas. | Tim King |
| 2012-10-30 | delta of a model-building failure case | Dejan Jovanović |
| 2012-10-29 | auflia directory missing from regression summary - fixed | Clark Barrett |
| 2012-10-26 | Fix to subrange type enumerator, and its unit test. Resolves bug 436. | Morgan Deters |
| 2012-10-26 | fixed bug in datatypes decision procedure enforcing rewriting of incorrectly ... | Andrew Reynolds |
| 2012-10-24 | fix for bug 429 | Dejan Jovanović |
| 2012-10-24 | two smaller random pure LRA push-pop cases that fail | Dejan Jovanović |
| 2012-10-23 | fixed problem with datatypes giving incorrect explanations, now corrected and... | Andrew Reynolds |
| 2012-10-22 | add bug 425 models regression; fix mac-build execute permission | Morgan Deters |
| 2012-10-11 | Fix bug 421, again, and add a second, independent test case for the same | Morgan Deters |
| 2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |
| 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 |
