summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2012-11-26fixup for incremental solvingDejan Jovanović
2012-11-26Removing DioSolver::acceptableOriginalNodes(). This assertion was too strong,...Tim King
2012-11-26Disabling test/regress/regress0/push-pop/bug396.smt2. This takes 2m to run in...Tim King
2012-11-25Adding a regression test from bug 462.Tim King
2012-11-23Example of rewrite rules use that comes from an harness testFrançois Bobot
2012-11-19Adding hand minimized test for bug 450.Tim King
2012-11-17Fixed last currently known bug in array modelsClark Barrett
2012-11-17* enable previously-failing (now succeeding) datatype example that uses recordsMorgan Deters
2012-11-17* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORT...Morgan Deters
2012-11-16Fix for bug451Clark Barrett
2012-11-15More fixes to model generation, with previously failing testcasesClark Barrett
2012-11-15fuzz15 should have been fuzz14Clark Barrett
2012-11-15Fix for bug 447.Tim King
2012-11-15Fixed another AUFBV model bug. BV equality subtheory needed to do somethingClark Barrett
2012-11-15Fixing comments in print_lambda.cvc.Tim King
2012-11-14Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ...Tim King
2012-11-14Fix to bug449. Adds shared constants to the set of DeltaRationals that must b...Tim King
2012-11-14bug fixes to models, array rewriter with previously failing testcasesClark Barrett
2012-11-13added support for division by zero for bit-vector division operatorsLiana Hadarean
2012-11-13Fixed an array rewriting bug found by fuzzerClark Barrett
2012-11-13Testcases for fixed bugsClark Barrett
2012-11-12Improved error reporting for improperly using non-linear division in linear a...Tim King
2012-11-12Delta is now generated in arithmetic to keep consistent the total order of De...Tim King
2012-11-10Fixed missing \ in uflra/Makefile.maClark Barrett
2012-11-10Fix for bug 439. Delta computation now includes disequality information.Tim King
2012-11-10Change run-regression script to *additionally* run a second test with --check...Morgan Deters
2012-11-10Updates to Clark's commit r4540:Morgan Deters
2012-11-09Test that breaks arithmetic model building due to disequality terms.Tim King
2012-11-09Arithmetic problem that fails --check-models due incompleteness with multipli...Tim King
2012-11-08Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases fo...Tim King
2012-11-08Review 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-07Fix to a bug in integer mod lemmas.Tim King
2012-10-30delta of a model-building failure caseDejan Jovanović
2012-10-29auflia directory missing from regression summary - fixedClark Barrett
2012-10-26Fix to subrange type enumerator, and its unit test. Resolves bug 436.Morgan Deters
2012-10-26fixed bug in datatypes decision procedure enforcing rewriting of incorrectly ...Andrew Reynolds
2012-10-24fix for bug 429 Dejan Jovanović
2012-10-24two smaller random pure LRA push-pop cases that failDejan Jovanović
2012-10-23fixed problem with datatypes giving incorrect explanations, now corrected and...Andrew Reynolds
2012-10-22add bug 425 models regression; fix mac-build execute permissionMorgan Deters
2012-10-11Fix bug 421, again, and add a second, independent test case for the sameMorgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-10Abstract values for SMT-LIB.Morgan Deters
2012-10-10fixing the cvc bv parser and typecheckerDejan Jovanović
2012-10-09* make Model class private (as discussed at meeting today)Morgan Deters
2012-10-09made datatypes rewrite incorrect selectors to ground term. this feature can ...Andrew Reynolds
2012-10-09fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 4...Morgan Deters
2012-10-08* Models' SubstitutionMaps are now attached to the user contextMorgan Deters
2012-10-08added reduced bv model failing test caseLiana Hadarean
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback