From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 12 Jun 2018 20:22:15 +0000 (-0500)
Subject: Fix strip constant endpoint for ITOS in strings rewriter (#2067)
X-Git-Tag: cvc5-1.0.0~4968
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b0a4253162ae4735f15540b41794f05f4f7f26f8;p=cvc5.git

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 a426c0306..78def9c0a 100644
--- 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 182f901ff..fd4a7da39 100644
--- 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
index 000000000..c8d8c5af3
--- /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)