From 78eea89ea7b92f28823f82d8c24ee5c982bf6c1c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 28 Jan 2019 23:58:40 -0800 Subject: update --- src/theory/strings/theory_strings_rewriter.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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(); -- cgit v1.2.3