Remove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 5 Jun 2021 03:22:57 +0000 (20:22 -0700)
committerGitHub <noreply@github.com>
Sat, 5 Jun 2021 03:22:57 +0000 (03:22 +0000)
commitf7b60f68bb6a7945eebb7f97a5f63302ad0ddc67
tree6490791cac69a8e112b74bafaab274916b722ce9
parent760874731c70e2aa32c3591c67a08f3ea85dcafd
Remove unwanted side effects in `SPLIT_EQ_STRIP_L` (#6689)

Fixes #6681. When checking whether SPLIT_EQ_STRIP_L applies, we were
using sripSymbolicLength, which changes its inputs depending on how
many elements of the concatenation it could strip. However, one of the
arguments, pfxv0, was reused across multiple checks if the strip did
not result in a rewrite. Later invocations were wrong as a result. This
commit changes the call to stripSymbolicLength() to use a new copy of
the vector instead.
src/theory/strings/sequences_rewriter.cpp
test/regress/CMakeLists.txt
test/regress/regress0/strings/issue6681-split-eq-strip-l.smt2 [new file with mode: 0644]