Make stripConstantEndpoints() less aggressive

`stripConstantEndpoints({ "A" }, { "A". (int.to.str n) }, {}, {}, 0)`
was cutting off "A" because it is a non-digit. This is wrong, however,
because `(int.to.str n)` can return the empty string. This commit
makes `stripConstantEndpoints()` less aggressive by not using
`str.to.int` terms to cut off non-digits anymore.

1 files changed, 0 insertions, 20 deletions

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 8d9d6a230..cbb298c5f 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -3683,26 +3683,6 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
             overlap = s.size() - ret;
           }
         }
-        else if (n2[index1].getKind() == kind::STRING_ITOS)
-        {
-          const std::vector<unsigned>& svec = s.getVec();
-          // can remove up to the first occurrence of a digit
-          unsigned svsize = svec.size();
-          for (unsigned i = 0; i < svsize; i++)
-          {
-            unsigned sindex = r == 0 ? i : (svsize - 1) - i;
-            if (String::isDigit(svec[sindex]))
-            {
-              break;
-            }
-            else if (sss.empty())  // only if not substr
-            {
-              // e.g. str.contains( str.++( "a", x ), int.to.str(y) ) -->
-              // str.contains( x, int.to.str(y) )
-              overlap--;
-            }
-          }
-        }
         else
         {
           // inconclusive