diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-23 14:59:20 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-23 12:59:20 -0700 |
| commit | 408bccf70b41b1f41c8be04ffe7f7002fb57e182 (patch) | |
| tree | a9a11516fd218ed9c8b99a8c289e3f39b9f82207 /src/theory/strings | |
| parent | 4dc48596188c0550e625434cdd893d909810f9de (diff) | |
Fixing some coverity warnings (#2357)
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index c777a0976..ce0100686 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2625,7 +2625,8 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form } if( !pinfer.empty() ){ //now, determine which of the possible inferences we want to add - int use_index = -1; + unsigned use_index = 0; + bool set_use_index = false; Trace("strings-solve") << "Possible inferences (" << pinfer.size() << ") : " << std::endl; unsigned min_id = 9; unsigned max_index = 0; @@ -2634,10 +2635,13 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form Trace("strings-solve") << "From " << pinfer[i].d_i << " / " << pinfer[i].d_j << " (rev=" << pinfer[i].d_rev << ") : "; Trace("strings-solve") << pinfer[i].d_conc << " by " << pinfer[i].d_id << std::endl; - if( use_index==-1 || pinfer[i].d_id<min_id || ( pinfer[i].d_id==min_id && pinfer[i].d_index>max_index ) ){ + if (!set_use_index || pinfer[i].d_id < min_id + || (pinfer[i].d_id == min_id && pinfer[i].d_index > max_index)) + { min_id = pinfer[i].d_id; max_index = pinfer[i].d_index; use_index = i; + set_use_index = true; } } //send the inference |