1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index f252196d8..861f7c694 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -25,10 +25,10 @@
 #include "theory/theory_model.h"
 
 using namespace std;
-using namespace CVC4::context;
-using namespace CVC4::kind;
+using namespace CVC5::context;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace strings {
 
@@ -48,7 +48,7 @@ RegExpSolver::RegExpSolver(SolverState& s,
       d_processed_memberships(s.getSatContext()),
       d_regexp_opr(skc)
 {
-  d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String(""));
+  d_emptyString = NodeManager::currentNM()->mkConst(::CVC5::String(""));
   std::vector<Node> nvec;
   d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_EMPTY, nvec);
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -582,7 +582,7 @@ bool RegExpSolver::checkPDerivative(
   return true;
 }
 
-CVC4::String RegExpSolver::getHeadConst(Node x)
+CVC5::String RegExpSolver::getHeadConst(Node x)
 {
   if (x.isConst())
   {
@@ -606,7 +606,7 @@ bool RegExpSolver::deriveRegExp(Node x,
   Assert(x != d_emptyString);
   Trace("regexp-derive") << "RegExpSolver::deriveRegExp: x=" << x
                          << ", r= " << r << std::endl;
-  CVC4::String s = getHeadConst(x);
+  CVC5::String s = getHeadConst(x);
   // only allow RE_DERIVE for concrete constant regular expressions
   if (!s.empty() && d_regexp_opr.getRegExpConstType(r) == RE_C_CONRETE_CONSTANT)
   {
@@ -615,7 +615,7 @@ bool RegExpSolver::deriveRegExp(Node x,
     bool flag = true;
     for (unsigned i = 0; i < s.size(); ++i)
     {
-      CVC4::String c = s.substr(i, 1);
+      CVC5::String c = s.substr(i, 1);
       Node dc2;
       int rt = d_regexp_opr.derivativeS(dc, c, dc2);
       dc = dc2;
@@ -706,4 +706,4 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp)
 
 }  // namespace strings
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5