Fix homogeneous string constant rewrite (#2545)

diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index f8bbeecf52ab883d70971acf61a6bce874379972..ad8591b3b6bd3c3e23433462fd993defc59004b1 100644 (file)
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -387,7 +387,7 @@ Node TheoryStringsRewriter::rewriteEqualityExt(Node node)
       unsigned hchar = 0;
       String lhss = node[i].getConst<String>();
       std::vector<unsigned> vec = lhss.getVec();
-      if (vec.size() > 1)
+      if (vec.size() >= 1)
       {
         hchar = vec[0];
         for (unsigned j = 1, size = vec.size(); j < size; j++)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5252954dcb5e5a970c72dd8e42cecb864f432286..cec33c61555b3253419e726cc53d73f0e326a5de 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -797,6 +797,7 @@ set(regress_0_tests
   regress0/strings/code-sat-neg-one.smt2
   regress0/strings/escchar.smt2
   regress0/strings/escchar_25.smt2
+  regress0/strings/hconst-092618.smt2
   regress0/strings/idof-rewrites.smt2
   regress0/strings/idof-sem.smt2
   regress0/strings/ilc-like.smt2

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 08d0ca5bb7d81893667081bd273aff2b8275662b..ce7bc87360f4e79c86da9c3432e3820be492da33 100644 (file)
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -807,6 +807,7 @@ REG0_TESTS = \
        regress0/strings/code-sat-neg-one.smt2 \
        regress0/strings/escchar.smt2 \
        regress0/strings/escchar_25.smt2 \
+       regress0/strings/hconst-092618.smt2 \
        regress0/strings/idof-rewrites.smt2 \
        regress0/strings/idof-sem.smt2 \
        regress0/strings/ilc-like.smt2 \

diff --git a/test/regress/regress0/strings/hconst-092618.smt2 b/test/regress/regress0/strings/hconst-092618.smt2
new file mode 100644 (file)
index 0000000..c7c5206
--- /dev/null
+++ b/test/regress/regress0/strings/hconst-092618.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(assert (str.contains "::" (str.++ x ":" x ":")))
+(check-sat)
\ No newline at end of file