Fix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites (#6550)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 17 May 2021 18:33:01 +0000 (11:33 -0700)
committerGitHub <noreply@github.com>
Mon, 17 May 2021 18:33:01 +0000 (18:33 +0000)
commit59d935b0210fe20cdddf5de2be91bb26a66d05fb
tree7d8d8b559a203834e7747e5b8a021ae85580e7d6
parentc20d3434af95f8cb8992dd3c70d0c30f1ba1495b
Fix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites (#6550)

Fixes #6520. The `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites were
applied too aggressively. Those rewrites attempt to rewrite string
equalities between concatenations where the prefix on one side is
provably shorter than the prefix on the other side. The length of the
shorter prefix is then stripped from the longer prefix. However, cvc5
was not checking whether it was able to strip the length of the full
prefix. If cvc5 cannot strip the full length of the shorter prefix, then
the rewrite does not apply because parts of the shorter prefix would
have to be kept. This commit adds an additional condition that checks
whether the length of the full prefix was stripped.
src/theory/strings/sequences_rewriter.cpp
test/regress/CMakeLists.txt
test/regress/regress0/strings/issue6520.smt2 [new file with mode: 0644]