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.

2 files changed, 31 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)
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;
+}