From: Tim King <taking@google.com>
Date: Mon, 26 Sep 2016 00:30:23 +0000 (-0700)
Subject: Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here.
X-Git-Tag: cvc5-1.0.0~6028^2~30
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=260c6cfecb47e1b426e982399d98e6e0d964a8e8;p=cvc5.git

Disambiguating a type issue. Coverity scan reported a MISMATCHED_ITERATOR here.
---

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));
             }
           }
         }