From: Tim King <taking@cs.nyu.edu>
Date: Mon, 11 Sep 2017 15:55:56 +0000 (-0700)
Subject: Addressing a coverity scan complaint in theory_strings.cpp. I believe the root cause... 
X-Git-Tag: cvc5-1.0.0~5648
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8465bf303d4a3b9edb4bf5601a727e9e29828d9;p=cvc5.git

Addressing a coverity scan complaint in theory_strings.cpp. I believe the root cause is that d_normal_forms_exp[r[0]] could have referred to different vectors (as operator[] is inserting for maps). (#1080)
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 412cc727d..c035fe7e4 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4008,7 +4008,8 @@ Node TheoryStrings::normalizeRegexp(Node r) {
             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());
+              const std::vector<Node>& r0_exp =  d_normal_forms_exp[r[0]];
+              nf_exp.insert(nf_exp.end(), r0_exp.begin(), r0_exp.end());
               nf_r = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, nf_r) );
             }
           }