Fix non-fixed length case in re-elim (#6612)

Fixes followup issues from #6604.

3 files changed, 19 insertions, 10 deletions

diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index c3580d963..f635cdc39 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -90,7 +90,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
   // into fixed length regular expressions are easy to handle.
   // the index of _* in re
   unsigned pivotIndex = 0;
-  size_t numPivotIndex = 0;
+  bool hasPivotIndex = false;
+  bool hasFixedLength = true;
   std::vector<Node> childLengths;
   std::vector<Node> childLengthsPostPivot;
   for (unsigned i = 0, size = children.size(); i < size; i++)
@@ -99,34 +100,34 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
     Node fl = RegExpEntail::getFixedLengthForRegexp(c);
     if (fl.isNull())
     {
-      if (numPivotIndex == 0 && c.getKind() == REGEXP_STAR
+      if (!hasPivotIndex && c.getKind() == REGEXP_STAR
           && c[0].getKind() == REGEXP_SIGMA)
       {
-        numPivotIndex = 1;
+        hasPivotIndex = true;
         pivotIndex = i;
         // zero is used in sum below and is used for concat-fixed-len
         fl = zero;
       }
       else
       {
-        numPivotIndex++;
+        hasFixedLength = false;
       }
     }
     if (!fl.isNull())
     {
       childLengths.push_back(fl);
-      if (numPivotIndex > 0)
+      if (hasPivotIndex)
       {
         childLengthsPostPivot.push_back(fl);
       }
     }
   }
-  Node lenSum = childLengths.size() > 1 ? nm->mkNode(PLUS, childLengths)
-                                        : childLengths[0];
-  // if we have at most one pivot index
-  if (numPivotIndex <= 1)
+  Node lenSum = childLengths.size() > 1
+                    ? nm->mkNode(PLUS, childLengths)
+                    : (childLengths.empty() ? zero : childLengths[0]);
+  // if we have a fixed length
+  if (hasFixedLength)
   {
-    bool hasPivotIndex = (numPivotIndex == 1);
     Assert(re.getNumChildren() == children.size());
     std::vector<Node> conc;
     conc.push_back(nm->mkNode(hasPivotIndex ? GEQ : EQUAL, lenx, lenSum));
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3d8016379..01deeaede 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2089,6 +2089,7 @@ set(regress_1_tests
   regress1/strings/issue6271-rnf.smt2
   regress1/strings/issue6271-2-rnf.smt2
   regress1/strings/issue6567-empty-re-range.smt2
+  regress1/strings/issue6604-2.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress1/strings/issue6604-2.smt2 b/test/regress/regress1/strings/issue6604-2.smt2
new file mode 100644
index 000000000..e28f5dcb5
--- /dev/null
+++ b/test/regress/regress1/strings/issue6604-2.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp --re-elim
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const a String)
+(assert (str.in_re a (re.++ (str.to_re "A") re.allchar (str.to_re "A"))))
+(assert (not (str.in_re a (re.++ (str.to_re "A") (re.* (re.++ (str.to_re "A") re.allchar)) re.allchar (str.to_re "A")))))
+(check-sat)