summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <noetzli@stanford.edu>2017-05-15 08:50:21 -0700
committerAndres Noetzli <noetzli@stanford.edu>2017-05-15 08:50:21 -0700
commit84af3731aa40e2e6f9281827af87350a2cb44ea1 (patch)
treeb159cbd1388df5afa23e14d1070ec812273b42c5
parent31681c7ff2a1469f5efc325fc1b3a406e3a85949 (diff)
Fix condition in upwards closure check for sets
Coverity reported this mismatched iterator.
-rw-r--r--src/theory/sets/theory_sets_private.cpp2
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback