summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2021-07-03 13:10:13 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2021-07-03 13:10:13 -0700
commitd89ab04b2d0a4dcd58a4fcec0431b78b08e1d001 (patch)
tree9af12feef4d53ace6831ba89e3a7a23b81493310 /src/theory/theory_engine.h
parent698d244a00618a0399bce9e15eddef52f68b8c94 (diff)
[Strings] Fix incorrect rewrite
Fixes #6834. There were two cases in our extended rewriter for string equalities that were modifying the node without returning and without updating information computed from the original node. This mismatch led to incorrect rewrites. This commit fixes the issue by adding a flag to `returnRewrite()` that determines whether node that was an equality before and after the rewrite should be rewritten again with the extended rewriter. We generally do not do that (we'd run in danger of rewriting equality nodes with the extended rewriter even though we shouldn't) but for the rewrites that were previously continuing to rewrite the node, we set this flag and return. This ensures that we do not have an issue with information being out of date. The commit additionally fixes an issue where we would apply the rewrite `STR_EQ_UNIFY` even though the node hadn't changed.
Diffstat (limited to 'src/theory/theory_engine.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback