From: Andres Noetzli <noetzli@stanford.edu>
Date: Mon, 15 May 2017 15:50:21 +0000 (-0700)
Subject: Fix condition in upwards closure check for sets
X-Git-Tag: cvc5-1.0.0~5800^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=84af3731aa40e2e6f9281827af87350a2cb44ea1;p=cvc5.git

Fix condition in upwards closure check for sets

Coverity reported this mismatched iterator.
---

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;