diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-09-16 13:36:05 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-16 15:36:05 -0500 |
| commit | 70bfc4f67bcad32fa1b9b581b71b3a2d70e14d7e (patch) | |
| tree | 3dc2c6217ad53dbf6a6fe889bb51b495a2a44e81 /test/api/CMakeLists.txt | |
| parent | 2c2f05c96e021006275a2bc70b9ede70b280616d (diff) | |
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.
Diffstat (limited to 'test/api/CMakeLists.txt')
| -rw-r--r-- | test/api/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index 8d9110e9f..9df87e9b5 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -34,6 +34,7 @@ cvc4_add_api_test(smt2_compliance) # TODO(cvc4-projects#209): Add methods for retrieving statistics to new API # cvc4_add_api_test(statistics) cvc4_add_api_test(two_solvers) +cvc4_add_api_test(issue5074) # if we've built using libedit, then we want the interactive shell tests if (USE_EDITLINE) |