Do not process looping word equations over sequences (#6434)

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 2abe2de8258fe1f99e871c6af04d707f2b378fe5..ed220c1eb3eb6bb684f83c97b783b0e8a1f4072b 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1771,23 +1771,27 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
                                                       int index,
                                                       CoreInferInfo& info)
 {
+  NodeManager* nm = NodeManager::currentNM();
+  Node conc;
+  const std::vector<Node>& veci = nfi.d_nf;
+  const std::vector<Node>& vecoi = nfj.d_nf;
+
+  TypeNode stype = veci[loop_index].getType();
+
   if (options::stringProcessLoopMode() == options::ProcessLoopMode::ABORT)
   {
     throw LogicException("Looping word equation encountered.");
   }
-  else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE)
+  else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE
+           || stype.isSequence())
   {
+    // note we cannot convert looping word equations into regular expressions if
+    // we are handling sequences, since there is no analog for regular
+    // expressions over sequences currently
     d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP);
     return ProcessLoopResult::SKIPPED;
   }
 
-  NodeManager* nm = NodeManager::currentNM();
-  Node conc;
-  const std::vector<Node>& veci = nfi.d_nf;
-  const std::vector<Node>& vecoi = nfj.d_nf;
-
-  TypeNode stype = veci[loop_index].getType();
-
   Trace("strings-loop") << "Detected possible loop for " << veci[loop_index]
                         << std::endl;
   Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl;