From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 21 Mar 2019 19:21:39 +0000 (-0500)
Subject:  Fix bad comparison in RE solver's addMembership (#2880)
X-Git-Tag: cvc5-1.0.0~4227
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a5466f262e16f3ebcd7c62df266a5ac0cd9c5b9a;p=cvc5.git

 Fix bad comparison in RE solver's addMembership (#2880)
---

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() ){