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/issue5074.cpp | |
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/issue5074.cpp')
-rw-r--r-- | test/api/issue5074.cpp | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/test/api/issue5074.cpp b/test/api/issue5074.cpp new file mode 100644 index 000000000..b39701f6b --- /dev/null +++ b/test/api/issue5074.cpp @@ -0,0 +1,30 @@ +/********************* */ +/*! \file issue5074.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Test for issue #5074 + **/ + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +int main() +{ + Solver slv; + Term c1 = slv.mkConst(slv.getIntegerSort()); + Term t6 = slv.mkTerm(Kind::STRING_FROM_CODE, c1); + Term t12 = slv.mkTerm(Kind::STRING_TO_REGEXP, t6); + Term t14 = slv.mkTerm(Kind::STRING_REPLACE_RE, {t6, t12, t6}); + Term t16 = slv.mkTerm(Kind::STRING_CONTAINS, {t14, t14}); + slv.checkEntailed(t16); + + return 0; +} |