From 9d98c926c971b70a04b8206e5b18c84b1dfeb38a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 26 Sep 2018 23:25:14 -0500 Subject: Fix homogeneous string constant rewrite (#2545) --- src/theory/strings/theory_strings_rewriter.cpp | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/Makefile.tests | 1 + test/regress/regress0/strings/hconst-092618.smt2 | 5 +++++ 4 files changed, 8 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/strings/hconst-092618.smt2 diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index f8bbeecf5..ad8591b3b 100644 --- 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(); std::vector 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 5252954dc..cec33c615 100644 --- 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 08d0ca5bb..ce7bc8736 100644 --- 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 index 000000000..c7c5206bd --- /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 -- cgit v1.2.3