From c74797f4cbded274e2dca6fee5e0efb439da03f5 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 22 Aug 2018 10:37:50 -0500
Subject: [PATCH] Fix invalid iterator comparisons (#2349)

---
 src/theory/quantifiers/conjecture_generator.cpp       |  9 ++++++---
 src/theory/quantifiers/fmf/bounded_integers.cpp       | 10 +++++-----
 src/theory/quantifiers/sygus/ce_guided_single_inv.cpp |  7 +++++--
 src/theory/sep/theory_sep.cpp                         |  4 +++-
 src/theory/sets/theory_sets_private.cpp               |  9 ++++++---
 5 files changed, 25 insertions(+), 14 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;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index f0789a503..8d8bf7f50 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -459,18 +459,18 @@ void BoundedIntegers::checkOwnership(Node f)
           success = true;
           //set Attributes on literals
           for( unsigned b=0; b<2; b++ ){
-            if (bound_lit_map[b].find(v) != bound_lit_map[b].end())
+            std::map<Node, Node>& blm = bound_lit_map[b];
+            if (blm.find(v) != blm.end())
             {
+              std::map<Node, bool>& blmp = bound_lit_pol_map[b];
               // WARNING_CANDIDATE:
               // This assertion may fail. We intentionally do not enable this in
               // production as it is considered safe for this to fail. We fail
               // the assertion in debug mode to have this instance raised to
               // our attention.
-              Assert(bound_lit_pol_map[b].find(v)
-                     != bound_lit_pol_map[b].end());
+              Assert(blmp.find(v) != blmp.end());
               BoundIntLitAttribute bila;
-              bound_lit_map[b][v].setAttribute(bila,
-                                               bound_lit_pol_map[b][v] ? 1 : 0);
+              bound_lit_map[b][v].setAttribute(bila, blmp[v] ? 1 : 0);
             }
             else
             {
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 5f5a84a6b..39c3baf5c 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -1036,8 +1036,11 @@ int TransitionInference::incrementTrace( DetTrace& dt, Node loc, bool fwd ) {
     }
   }
   if( fwd ){
-    std::map< Node, std::map< Node, Node > >::iterator it = d_com[0].d_const_eq.find( loc );
-    if( it!=d_com[0].d_const_eq.end() ){
+    Component& cm = d_com[0];
+    std::map<Node, std::map<Node, Node> >::iterator it =
+        cm.d_const_eq.find(loc);
+    if (it != cm.d_const_eq.end())
+    {
       std::vector< Node > next;
       for( unsigned i=0; i<d_prime_vars.size(); i++ ){
         Node pv = d_prime_vars[i];
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 6c9c34123..6085b1f23 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -646,7 +646,9 @@ void TheorySep::check(Effort e) {
             if( assert_active[fact] ){
               Assert( atom.getKind()==kind::SEP_LABEL );
               TNode s_lbl = atom[1];
-              if( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){
+              std::map<Node, std::map<int, Node> >& lms = d_label_map[s_atom];
+              if (lms.find(s_lbl) != lms.end())
+              {
                 Trace("sep-process-debug") << "Active lbl : " << s_lbl << std::endl;
                 active_lbl[s_lbl] = true;
               }
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 9346970d1..ab9fa6d54 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -611,11 +611,14 @@ void TheorySetsPrivate::fullEffortCheck(){
           }else{
             Node r1 = d_equalityEngine.getRepresentative( n[0] );
             Node r2 = d_equalityEngine.getRepresentative( n[1] );
-            if( d_bop_index[n.getKind()][r1].find( r2 )==d_bop_index[n.getKind()][r1].end() ){
-              d_bop_index[n.getKind()][r1][r2] = n;
+            std::map<Node, Node>& binr1 = d_bop_index[n.getKind()][r1];
+            std::map<Node, Node>::iterator itb = binr1.find(r2);
+            if (itb == binr1.end())
+            {
+              binr1[r2] = n;
               d_op_list[n.getKind()].push_back( n );
             }else{
-              d_congruent[n] = d_bop_index[n.getKind()][r1][r2];
+              d_congruent[n] = itb->second;
             }
           }
           d_nvar_sets[eqc].push_back( n );
-- 
2.30.2