diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-11 11:58:46 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-11 11:58:46 -0700 |
commit | 9e31c2e071bf210055e087fc77b16ad2d3ec8b29 (patch) | |
tree | c1e38828ec5843751f20f0c7704dcad51d729eb0 | |
parent | 6ae63e11bf6b8cfa50e29e9ace43056c75d605fc (diff) |
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 712029283..6ee01e992 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2493,7 +2493,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // Collect the equalities of the form (= x "") (sorted) std::set<TNode> emptyNodes; - bool allEqs = true; + bool allEmptyEqs = true; if (cmp_conr.getKind() == kind::EQUAL) { if (cmp_conr[0] == empty) @@ -2504,6 +2504,10 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { { emptyNodes.insert(cmp_conr[0]); } + else + { + allEmptyEqs = false; + } } else { @@ -2522,7 +2526,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { } else { - allEqs = false; + allEmptyEqs = false; } } } @@ -2541,7 +2545,7 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // // (str.replace "" y z) ---> (str.replace "" (str.++ y1 ... yn) z) // if (str.contains "" y) ---> (and (= y1 "") ... (= yn "")) - if (node[0] == empty && allEqs) + if (node[0] == empty && allEmptyEqs) { std::vector<Node> emptyNodesList(emptyNodes.begin(), emptyNodes.end()); Node nn1 = mkConcat(STRING_CONCAT, emptyNodesList); |