diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-28 23:58:40 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-28 23:58:40 -0800 |
commit | 78eea89ea7b92f28823f82d8c24ee5c982bf6c1c (patch) | |
tree | 3ed552cb4af3da81c5a813803b71fa89ee364d0d | |
parent | 00b211809a8251a95dc7aa0f64f48cc5dd7f60b9 (diff) |
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 689f0688c..d3bb42e69 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -512,7 +512,7 @@ Node TheoryStringsRewriter::rewriteStrEqualityExt(Node node) } // (= "" (str.substr "A" 0 z)) ---> (<= z 0) - if (checkEntailNonEmpty(ne[0]) && ne[1] == zero) + if (checkEntailArith(nm->mkNode(STRING_LENGTH, ne[0]), ne[1], true)) //checkEntailNonEmpty(ne[0]) && ne[1] == zero) { Node ret = nm->mkNode(LEQ, ne[2], zero); return returnRewrite(node, ret, "str-emp-substr-leq-z"); @@ -5145,6 +5145,8 @@ Node TheoryStringsRewriter::returnRewrite(Node node, Node ret, const char* c) { Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << c << "." << std::endl; + //std::cout << "Rewrite " << node << " to " << ret << " by " << c + // << "." << std::endl; NodeManager* nm = NodeManager::currentNM(); |