projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cc726b5) | patch
bug 168 fixed (TheoryEngine::rewrite is not fully rewriting to a fix point); problem...
authorMorgan Deters <mdeters@gmail.com>
Sun, 4 Jul 2010 02:18:02 +0000 (02:18 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sun, 4 Jul 2010 02:18:02 +0000 (02:18 +0000)
commit994427c682dfe7323a0e806b18095b862508d454
tree3ceec8e2a122d8d769b29b6395b5e4fb1aac099dtree
parentcc726b5080f8926a3cb96a1b9d1098ad8725ab86commit | diff
bug 168 fixed (TheoryEngine::rewrite is not fully rewriting to a fix point); problem had to do with the builtin theory post-rewriting DISTINCT into an arithmetic term not in normal form.  fix was to do DISTINCT rewriting in pre-rewrite.  note that this doesn't add to the amount of theory rewriting work that needs to be done, because everything is cached
src/theory/builtin/theory_builtin.cpp diff | blob | history
src/theory/builtin/theory_builtin.h diff | blob | history