summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Fixes for two bugs:Morgan Deters
2013-04-01Adding tests for the previous commit.Tim King
2013-04-01Merging some cleanup work:Morgan Deters
2013-04-01Fix for iff terms over equalities between the same term and differing constants.Tim King
2013-04-01Fix bug 491 and related issues with checkModel() and quantifiers. Enabling p...Morgan Deters
2013-04-01fixed TheoryBool rewriter buglianah
2013-03-26added model generation for bv subtheories and bv-inequality solver optionlianah
2013-03-23non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)lianah
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-21Some model and printing fixes for defined functions in input.Morgan Deters
2013-03-21added regression test for constant evallianah
2013-03-21Merge branch 'master' into bv-corelianah
2013-03-20added more testslianah
2013-03-20generalized bv inequality reasoning to handle both strict and non-strict ineq...lianah
2013-03-20Fix to bug 497: make justification heuristic's ITE cache context-dependent.Morgan Deters
2013-03-20Interactive mode support for multiline inputMorgan Deters
2013-03-20Properly |quote| symbols in SMT-LIBv2 output.Morgan Deters
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-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds an...Morgan Deters
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-04Merge branch '1.0.x'Morgan Deters
2013-02-04Fix NodeBuilder bug which could attempt to allocate beyond hard limitMorgan 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback