From a5466f262e16f3ebcd7c62df266a5ac0cd9c5b9a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 21 Mar 2019 14:21:39 -0500
Subject: [PATCH]  Fix bad comparison in RE solver's addMembership (#2880)

---
 src/theory/strings/theory_strings.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6300345ae..c84ae404a 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -5108,7 +5108,8 @@ void TheoryStrings::addMembership(Node assertion) {
   if(polarity) {
     int index = 0;
     NodeIntMap::const_iterator it = d_pos_memberships.find( x );
-    if( it!=d_nf_pairs.end() ){
+    if (it != d_pos_memberships.end())
+    {
       index = (*it).second;
       for( int k=0; k<index; k++ ){
         if( k<(int)d_pos_memberships_data[x].size() ){
@@ -5134,7 +5135,8 @@ void TheoryStrings::addMembership(Node assertion) {
     }*/
     int index = 0;
     NodeIntMap::const_iterator it = d_neg_memberships.find( x );
-    if( it!=d_nf_pairs.end() ){
+    if (it != d_neg_memberships.end())
+    {
       index = (*it).second;
       for( int k=0; k<index; k++ ){
         if( k<(int)d_neg_memberships_data[x].size() ){
-- 
2.30.2