projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f4b167e) | patch
[BV] Fix response of `RewriteConcat` (#8074)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 7 Feb 2022 20:00:49 +0000 (12:00 -0800)
committerGitHub <noreply@github.com>
Mon, 7 Feb 2022 20:00:49 +0000 (20:00 +0000)
commit67708218de9a83f395daabea57f8f0a9643c2e7a
tree4420d9d63bbb6e99d72063ebbf6bbebfb5e0661dtree
parentf4b167eb29e2716e996450d844a8bd4de626d7f6commit | diff
[BV] Fix response of `RewriteConcat` (#8074)

RewriteConcat was returning REWRITE_DONE, but it could happen that
applying ExtractWhole was removing an extract around another
concat that could then be flattened (see added unit test for an
example). This commit makes the response more conservative and only
returns REWRITE_DONE if the node did not change.
src/theory/bv/theory_bv_rewriter.cpp diff | blob | history
test/unit/theory/theory_bv_rewriter_white.cpp diff | blob | history