Only apply testConstStringInRegExp to const regexp (#4120)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 19 Mar 2020 14:18:58 +0000 (07:18 -0700)
committerGitHub <noreply@github.com>
Thu, 19 Mar 2020 14:18:58 +0000 (09:18 -0500)
commit089a60266f2658e471d204fdd737e3e0d37e105c
treedd07799cf5a1a06f184ce402fab016bf54c656e0
parent94844fbf4fbe4fa08d8fa4cbe093ba532f5bd613
Only apply testConstStringInRegExp to const regexp (#4120)

Fixes #4070. `TheoryStringsRewriter::rewriteConcatRegExp()` rewrites
`(a)* ++ (_)*` to `(_)*`. To do so, it checks whether the elements
preceding `(_)*` match the empty string using
`TheoryStringsRewriter::testConstStringInRegExp()`. However, this method
only expects to be called on constant regular expressions (i.e. regular
expressions without string variables). This commit adds a corresponding
check before calling `TheoryStringsRewriter::testConstStringInRegExp()`.
src/theory/strings/theory_strings_rewriter.cpp
test/regress/CMakeLists.txt
test/regress/regress0/strings/issue4070.smt2 [new file with mode: 0644]
test/unit/theory/theory_strings_rewriter_white.h