summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Expand)Author
2013-09-11Theory of strings.Tianyi Liang
2013-09-09Another minor fix for datatypes to repair my previous commit.Andrew Reynolds
2013-09-09Support empty (and 1-ary) tuples and records.Morgan Deters
2013-08-26Merge branch '1.2.x'Kshitij Bansal
2013-08-26bug 374 fix: assert litVal=desiredVal only for leaf nodes1.2.xKshitij Bansal
2013-08-26Bug 374 benchmarksKshitij Bansal
2013-07-19enable bug521 regression testsMorgan Deters
2013-07-17Fix bug 516; include some bug testcases.Morgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
2013-07-09Fix for bug 519; don't involve ITESimplifier in model generation.Morgan Deters
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-06-04Merge branch '1.2.x'Morgan Deters
2013-06-04Fix clang static initialization order issue; fixes bug 512.Morgan Deters
2013-05-22Add regressions for finite model findingAndrew Reynolds
2013-05-21Merge branch '1.2.x'Morgan Deters
2013-05-21Fix bug 512: an assertion failure only appearing with clang on Mac OS, due to...Morgan Deters
2013-05-21Merge branch '1.2.x'Morgan Deters
2013-05-21Fix incremental bug in symmetry breaker.Morgan Deters
2013-05-20Fix for equality-chaining of Booleans in SMT-LIBv2.Morgan Deters
2013-05-17Fix for equality-chaining of Booleans in SMT-LIBv2.Morgan Deters
2013-05-09Changing the integer normal form to increase matching.Tim King
2013-05-07fix for bug500Dejan Jovanović
2013-05-01Fix to boolean-terms; resolves bug #507Morgan Deters
2013-04-26Merge experimental decisionweight branchKshitij Bansal
2013-04-26FCSimplex branch mergeTim King
2013-04-17boolean flatten: bug fix in dfs searchKshitij Bansal
2013-04-16generalize to handle andKshitij Bansal
2013-04-16flatten or nodesKshitij Bansal
2013-04-03Some final minor changes before cutting 1.1.Morgan 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-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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback