diff options
author | Tim King <taking@google.com> | 2016-09-25 17:30:23 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-09-25 17:30:23 -0700 |
commit | 260c6cfecb47e1b426e982399d98e6e0d964a8e8 (patch) | |
tree | ffcbf91ed420f3a3f608813651f9ec3b8472a72d | |
parent | 54461798bc0ae519ebe11cee370d42b58a2fecd2 (diff) |
Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here.
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0062028fe..2f6f7e9e7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3974,11 +3974,17 @@ Node TheoryStrings::normalizeRegexp(Node r) { if(r[0].isConst()) { break; } else { - if(d_normal_forms.find( r[0] ) != d_normal_forms.end()) { - nf_r = mkConcat( d_normal_forms[r[0]] ); - Debug("regexp-nf") << "Term: " << r[0] << " has a normal form " << nf_r << std::endl; - nf_exp.insert(nf_exp.end(), d_normal_forms_exp[r[0]].begin(), d_normal_forms_exp[r[0]].end()); - nf_r = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, nf_r) ); + if (d_normal_forms.find(r[0]) != d_normal_forms.end()) { + const std::vector<Node>& nf_r0 = d_normal_forms[r[0]]; + nf_r = mkConcat(nf_r0); + Debug("regexp-nf") << "Term: " << r[0] << " has a normal form " + << nf_r << std::endl; + std::vector<Node>::iterator nf_end_exp = nf_exp.end(); + std::vector<Node>::const_iterator nf_r0_begin = nf_r0.begin(); + std::vector<Node>::const_iterator nf_r0_end = nf_r0.end(); + nf_exp.insert(nf_end_exp, nf_r0_begin, nf_r0_end); + nf_r = Rewriter::rewrite(NodeManager::currentNM()->mkNode( + kind::STRING_TO_REGEXP, nf_r)); } } } |