From 84af3731aa40e2e6f9281827af87350a2cb44ea1 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 15 May 2017 08:50:21 -0700 Subject: [PATCH] Fix condition in upwards closure check for sets Coverity reported this mismatched iterator. --- src/theory/sets/theory_sets_private.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; -- 2.30.2