diff options
Diffstat (limited to 'src/theory/strings/theory_strings_rewriter.cpp')
| -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(); |