Fix invalid iterator comparisons (#2349)

1 files changed, 6 insertions, 3 deletions

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 );