diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2017-05-15 08:50:21 -0700 |
---|---|---|
committer | Andres Noetzli <noetzli@stanford.edu> | 2017-05-15 08:50:21 -0700 |
commit | 84af3731aa40e2e6f9281827af87350a2cb44ea1 (patch) | |
tree | b159cbd1388df5afa23e14d1070ec812273b42c5 /src/theory/sets | |
parent | 31681c7ff2a1469f5efc325fc1b3a406e3a85949 (diff) |
Fix condition in upwards closure check for sets
Coverity reported this mismatched iterator.
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 0338eb1b3..a0748f2b9 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -856,7 +856,7 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) { valid = true; }else{ // if not, check whether it is definitely not a member, if unknown, split - bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2->second.end(); + bool not_in_r2 = itm2n!=d_pol_mems[1].end() && itm2n->second.find( xr )!=itm2n->second.end(); if( !not_in_r2 ){ exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ) ); valid = true; |