Fix invalid iterator comparisons (#2349)

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;