summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Expand)Author
2013-03-20one more ineq regressionLiana Hadarean
2013-03-19fixed reversed concat in core theoryLiana Hadarean
2013-03-19merged master with dejan's constant evaluating equality engineLiana Hadarean
2013-03-19inequality reasoning works on small examples added to regressions (not increm...Liana Hadarean
2013-03-19Fixes for miplib-trick application (and a new testcase)Morgan Deters
2013-03-16started work on the inequality bv subtheorylianah
2013-02-26Merge branch '1.0.x'lianah
2013-02-26fix for bv crash in incremental mode; this is a temporary fix for bug 493lianah
2013-02-16Some cleanup and copyright updatingMorgan Deters
2013-02-07Merge branch '1.0.x'Morgan Deters
2013-02-07Significant work on bug #491 (not yet closed).Morgan Deters
2013-02-07More complete fix for bug 484 (includes fixes for records and tuples).Morgan Deters
2013-02-05Fix to miplib trick to make it less "cautious" and apply in more casesMorgan Deters
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed b...Andrew Reynolds
2013-02-03Some cleanup of miplib regressions and optionsMorgan Deters
2013-02-03Merge from mdeters/miplib branch (commit 'ce7c485182902ae43871057185095f71f74...Morgan Deters
2013-02-03new miplib pass, works for 1 or 2 varsMorgan Deters
2013-02-01Merge branch '1.0.x'Morgan Deters
2013-02-01Fix a tuple attribute bug that was causing model-generation problems for tuplesMorgan Deters
2013-01-29currently disabling bug486 regression. we need to discuss getValue/collectMo...Andrew Reynolds
2013-01-28Fix the regression test for bug 486, and enable itMorgan Deters
2013-01-28Fix the regression test for bug 486, and enable itMorgan Deters
2013-01-28some fixes for win32, including ability to "make check" win32 builds via wineMorgan Deters
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2013-01-08SMT-LIB get-model output now is easier to machine-parse: contains (model...) ...Morgan Deters
2012-12-11SMT-LIB compliance fix to get-assignment; resolves bug 480Morgan Deters
2012-12-06Fix for fuzzer-found model bugClark Barrett
2012-12-01remove an obsolete (and incorrect) assertion in boolean-terms; also add faili...Morgan Deters
2012-12-01Some fixes for boolean arraysMorgan Deters
2012-11-30Add some regressions for bug 438.Morgan Deters
2012-11-30fix rewrite-rules syntax in regressionMorgan Deters
2012-11-30fix the syntax of assert-rewrite/-propagation/-reduction by putting the patte...François Bobot
2012-11-29reliable benchmark corresponding to bug468Kshitij Bansal
2012-11-27Functions and predicates over Boolean now work with --check-models and output...Morgan Deters
2012-11-27First chunk of boolean-terms support.Morgan Deters
2012-11-27Tuples and records merge. Resolves bug 270.Morgan Deters
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-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-15Fixed another AUFBV model bug. BV equality subtheory needed to do somethingClark Barrett
2012-11-15Fixing comments in print_lambda.cvc.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback