From 260c6cfecb47e1b426e982399d98e6e0d964a8e8 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 25 Sep 2016 17:30:23 -0700 Subject: [PATCH] Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here. --- src/theory/strings/theory_strings.cpp | 16 +++++++++++----- 1 file 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& 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::iterator nf_end_exp = nf_exp.end(); + std::vector::const_iterator nf_r0_begin = nf_r0.begin(); + std::vector::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)); } } } -- 2.30.2