diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-22 10:37:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-22 10:37:50 -0500 |
commit | c74797f4cbded274e2dca6fee5e0efb439da03f5 (patch) | |
tree | 54b54a1e9e468dec4d97673e03be473632ed1549 /src/theory/quantifiers/conjecture_generator.cpp | |
parent | ab8d44b83e210ed38623a1440e3ef1d318f7d0d0 (diff) |
Fix invalid iterator comparisons (#2349)
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index a079017cd..e82ab617a 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -882,9 +882,12 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in d_conj_count++; }else{ std::vector< Node > bvs; - for( std::map< TypeNode, unsigned >::iterator it = d_pattern_var_id[lhs].begin(); it != d_pattern_var_id[lhs].end(); ++it ){ - for( unsigned i=0; i<=it->second; i++ ){ - bvs.push_back( getFreeVar( it->first, i ) ); + for (const std::pair<TypeNode, unsigned>& lhs_pattern : + d_pattern_var_id[lhs]) + { + for (unsigned i = 0; i <= lhs_pattern.second; i++) + { + bvs.push_back(getFreeVar(lhs_pattern.first, i)); } } Node rsg; |