diff options
| -rw-r--r-- | src/theory/strings/strings_entail.cpp | 14 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue4701_substr_splice.smt2 | 12 |
3 files changed, 25 insertions, 2 deletions
diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index 928414523..b2c2c3cd3 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -225,6 +225,9 @@ int StringsEntail::componentContains(std::vector<Node>& n1, { Assert(nb.empty()); Assert(ne.empty()); + Trace("strings-entail") << "Component contains: " << std::endl; + Trace("strings-entail") << "n1 = " << n1 << std::endl; + Trace("strings-entail") << "n2 = " << n2 << std::endl; // if n2 is a singleton, we can do optimized version here if (n2.size() == 1) { @@ -301,6 +304,10 @@ int StringsEntail::componentContains(std::vector<Node>& n1, -1, computeRemainder && remainderDir != -1)) { + Trace("strings-entail-debug") + << "Last remainder begin is " << n1rb_last << std::endl; + Trace("strings-entail-debug") + << "Last remainder end is " << n1re_last << std::endl; Assert(n1rb_last.isNull()); if (computeRemainder) { @@ -325,6 +332,9 @@ int StringsEntail::componentContains(std::vector<Node>& n1, } } } + Trace("strings-entail-debug") << "ne = " << ne << std::endl; + Trace("strings-entail-debug") << "nb = " << nb << std::endl; + Trace("strings-entail-debug") << "...return " << i << std::endl; return i; } else @@ -444,12 +454,12 @@ bool StringsEntail::componentContainsBase( { return false; } - if (dir != 1) + if (dir != -1) { n1rb = nm->mkNode( STRING_SUBSTR, n2[0], nm->mkConst(Rational(0)), start_pos); } - if (dir != -1) + if (dir != 1) { n1re = nm->mkNode(STRING_SUBSTR, n2[0], end_pos, len_n2s); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 95c272a3e..a0fee2185 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1808,6 +1808,7 @@ set(regress_1_tests regress1/strings/issue3657-unexpectedUnsatCVC4.smt2 regress1/strings/issue4379.smt2 regress1/strings/issue4608-re-derive.smt2 + regress1/strings/issue4701_substr_splice.smt2 regress1/strings/issue4735.smt2 regress1/strings/issue4735_2.smt2 regress1/strings/issue4759-comp-delta.smt2 diff --git a/test/regress/regress1/strings/issue4701_substr_splice.smt2 b/test/regress/regress1/strings/issue4701_substr_splice.smt2 new file mode 100644 index 000000000..28e89588f --- /dev/null +++ b/test/regress/regress1/strings/issue4701_substr_splice.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_SLIA) +(set-info :status sat) +(set-option :strings-exp true) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(declare-fun e () String) +(assert (= e (str.++ b (str.substr a 0 1)))) +(assert (= a (str.substr c 0 (str.len e)))) +(assert (= "a" b)) +(assert (= (str.++ b a) (str.replace c e a))) +(check-sat) |