[Strings] Fix incorrect rewrite (#6837)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 5 Jul 2021 13:29:09 +0000 (06:29 -0700)
committerGitHub <noreply@github.com>
Mon, 5 Jul 2021 13:29:09 +0000 (13:29 +0000)
commitadf5216eff4e75dd9c5d08fce3bfc2161250c86e
tree3add3b59f08d5ef9006ce68a48142fd352620dad
parentdbf823ab9c0fa1ed3b5ab6e165625c3d3993d65f
[Strings] Fix incorrect rewrite (#6837)

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.
src/theory/strings/sequences_rewriter.cpp
src/theory/strings/sequences_rewriter.h
test/regress/CMakeLists.txt
test/regress/regress0/strings/issue6834-str-eq-const-nhomog.smt2 [new file with mode: 0644]