projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c1fa821) | patch
Fix rewrite for `str.update(str.rev(s), n, t))` (#7838)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 17 Dec 2021 21:46:14 +0000 (13:46 -0800)
committerGitHub <noreply@github.com>
Fri, 17 Dec 2021 21:46:14 +0000 (21:46 +0000)
commit2df0cc4257391daf6daf175826d69a735517ad19
treea13140710db07242c55d99b6601261d82f7db2e0tree
parentc1fa82197bfec2bfb3f8655ebfde546d085e0fe4commit | diff
Fix rewrite for `str.update(str.rev(s), n, t))` (#7838)

Fixes https://github.com/cvc5/cvc5-projects/issues/390. This commit
fixes two issues with the rewrite: (1) the rewrite should only apply if
the update is of size 1 and (2) the `str.rev(...)` should be removed
inside the `str.update(...)`.
src/theory/strings/sequences_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/proj-issue390-update-rev-rewrite.smt2 [new file with mode: 0644] blob