Fix type error with regexp (#1778)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 142695b9dd59e735199be35bc549d55725b9999b..713c346e04810fcc4b0f01d298a62058b4cf3935 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4621,33 +4621,18 @@ Node TheoryStrings::getNormalSymRegExp(Node r, std::vector<Node> &nf_exp) {
       }
       break;
     }
-    case kind::REGEXP_CONCAT: {
-      std::vector< Node > vec_nodes;
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
-      }
-      ret = mkConcat(vec_nodes);
-      break;
-    }
-    case kind::REGEXP_UNION: {
-      std::vector< Node > vec_nodes;
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
-      }
-      ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, vec_nodes) );
-      break;
-    }
-    case kind::REGEXP_INTER: {
+    case kind::REGEXP_CONCAT:
+    case kind::REGEXP_UNION:
+    case kind::REGEXP_INTER:
+    case kind::REGEXP_STAR:
+    {
       std::vector< Node > vec_nodes;
-      for(unsigned i=0; i<r.getNumChildren(); ++i) {
-        vec_nodes.push_back( getNormalSymRegExp(r[i], nf_exp) );
+      for (const Node& cr : r)
+      {
+        vec_nodes.push_back(getNormalSymRegExp(cr, nf_exp));
       }
-      ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_INTER, vec_nodes) );
-      break;
-    }
-    case kind::REGEXP_STAR: {
-      ret = getNormalSymRegExp( r[0], nf_exp );
-      ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, ret) );
+      ret = Rewriter::rewrite(
+          NodeManager::currentNM()->mkNode(r.getKind(), vec_nodes));
       break;
     }
     //case kind::REGEXP_PLUS: