1 files changed, 7 insertions, 12 deletions
diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index aa69f9ecf..c2ee079db 100644
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -28,7 +28,7 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-RegExpEntail::RegExpEntail(Rewriter* r) : d_rewriter(r), d_aent(r)
+RegExpEntail::RegExpEntail(Rewriter* r) : d_aent(r)
 {
   d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
   d_one = NodeManager::currentNM()->mkConstInt(Rational(1));
@@ -659,11 +659,9 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n)
   Kind k = n.getKind();
   if (k == STRING_TO_REGEXP)
   {
-    Node ret = nm->mkNode(STRING_LENGTH, n[0]);
-    ret = Rewriter::rewrite(ret);
-    if (ret.isConst())
+    if (n[0].isConst())
     {
-      return ret;
+      return nm->mkConstInt(Rational(Word::getLength(n[0])));
     }
   }
   else if (k == REGEXP_ALLCHAR || k == REGEXP_RANGE)
@@ -690,7 +688,7 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n)
   }
   else if (k == REGEXP_CONCAT)
   {
-    NodeBuilder nb(PLUS);
+    Rational sum(0);
     for (const Node& nc : n)
     {
       Node flc = getFixedLengthForRegexp(nc);
@@ -698,11 +696,10 @@ Node RegExpEntail::getFixedLengthForRegexp(TNode n)
       {
         return flc;
       }
-      nb << flc;
+      Assert(flc.isConst() && flc.getType().isInteger());
+      sum += flc.getConst<Rational>();
     }
-    Node ret = nb.constructNode();
-    ret = Rewriter::rewrite(ret);
-    return ret;
+    return nm->mkConstInt(sum);
   }
   return Node::null();
 }
@@ -785,8 +782,6 @@ Node RegExpEntail::getConstantBoundLengthForRegexp(TNode n, bool isLower) const
 
 bool RegExpEntail::regExpIncludes(Node r1, Node r2)
 {
-  Assert(Rewriter::rewrite(r1) == r1);
-  Assert(Rewriter::rewrite(r2) == r2);
   if (r1 == r2)
   {
     return true;