Fix strip constant endpoint for ITOS in strings rewriter (#2067)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index a426c0306bcfa3279a4e25739b41a0453f59d43f..78def9c0a56137d74baf00fd77d34307dfcf983f 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -2915,9 +2915,10 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1,
         {
           const std::vector<unsigned>& svec = s.getVec();
           // can remove up to the first occurrence of a digit
-          for (unsigned i = 0; i < svec.size(); i++)
+          unsigned svsize = svec.size();
+          for (unsigned i = 0; i < svsize; i++)
           {
-            unsigned sindex = r == 0 ? i : svec.size() - i;
+            unsigned sindex = r == 0 ? i : (svsize - 1) - i;
             if (String::isDigit(svec[sindex]))
             {
               break;

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 182f901ff0d9d1bf12cd0496176db3e47bc70a85..fd4a7da399d11aa4470c19df48126c2082d20739 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -806,6 +806,7 @@ REG0_TESTS = \
        regress0/strings/str005.smt2 \
        regress0/strings/strings-charat.cvc \
        regress0/strings/strings-native-simple.cvc \
+       regress0/strings/strip-endpoint-itos.smt2 \
        regress0/strings/substr-rewrites.smt2 \
        regress0/strings/type001.smt2 \
        regress0/strings/unsound-0908.smt2 \

diff --git a/test/regress/regress0/strings/strip-endpoint-itos.smt2 b/test/regress/regress0/strings/strip-endpoint-itos.smt2
new file mode 100644 (file)
index 0000000..c8d8c5a
--- /dev/null
+++ b/test/regress/regress0/strings/strip-endpoint-itos.smt2
@@ -0,0 +1,7 @@
+(set-info :smt-lib-version 2.5)
+(set-logic QF_SLIA)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun x () Int)
+(assert (str.contains "Ducati100" (int.to.str x)))
+(check-sat)