Only rewrite replace_re(_all) if regexp is const (#5075)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 16 Sep 2020 20:36:05 +0000 (13:36 -0700)
committerGitHub <noreply@github.com>
Wed, 16 Sep 2020 20:36:05 +0000 (15:36 -0500)
commit70bfc4f67bcad32fa1b9b581b71b3a2d70e14d7e
tree3dc2c6217ad53dbf6a6fe889bb51b495a2a44e81
parent2c2f05c96e021006275a2bc70b9ede70b280616d
Only rewrite replace_re(_all) if regexp is const (#5075)

Fixes #5074. This commit fixes an issue in the rewriter of
str.replace_re and str.replace_re_all. For both operators, we do two
kinds of rewrites: (1) If the first argument is a constant, then we
check whether the regular expression appears in that constant and (2) we
check whether the regular expression matches the empty string. Both of
those checks were assuming a constant regular expression but there was
no guard in place for it. This commit adds the missing guard.
src/theory/strings/sequences_rewriter.cpp
test/api/CMakeLists.txt
test/api/issue5074.cpp [new file with mode: 0644]