Fix corner case in stripConstantEndpoints (#2824)

`stripConstantEndpoints()` was returning `true` when the first argument
was a list only containing an empty string, which could lead to rewrite
loops. This commit checks for that case and adds a unit test for it.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 0c8d6ac8d..f90d5bcfd 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3583,6 +3583,12 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
       unsigned index1 = r == 0 ? 0 : n2.size() - 1;
       bool removeComponent = false;
       Node n1cmp = n1[index0];
+
+      if (n1cmp.isConst() && n1cmp.getConst<String>().size() == 0)
+      {
+        return false;
+      }
+
       std::vector<Node> sss;
       std::vector<Node> sls;
       n1cmp = decomposeSubstrChain(n1cmp, sss, sls);