diff options
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 2 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
-rw-r--r-- | test/regress/regress0/strings/hconst-092618.smt2 | 5 |
4 files changed, 8 insertions, 1 deletions
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<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 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 |