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/sets | |
parent | ab8d44b83e210ed38623a1440e3ef1d318f7d0d0 (diff) |
Fix invalid iterator comparisons (#2349)
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 9 |
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 ); |