From: PaulMeng <baolmeng@gmail.com>
Date: Tue, 22 Mar 2016 02:09:27 +0000 (-0500)
Subject: minor fix
X-Git-Tag: cvc5-1.0.0~6067
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=030f39b6a65d1488bb41db1daa387d8859251b7b;p=cvc5.git

minor fix
---

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 42473e4f2..fc1c1c666 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -83,9 +83,11 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
           }
           if(kind_terms.find(kind::JOIN) != kind_terms.end()) {
             std::vector<Node> join_terms = kind_terms[kind::JOIN];
+            Trace("rels-debug") << "[sets-rels] apply join rules on join terms with size = " << join_terms.size() << std::endl;
             // exp is a membership term and join_terms contains all
             // terms involving "join" operator that are in the same equivalence class with the right hand side of exp
             for(unsigned int j = 0; j < join_terms.size(); j++) {
+              Trace("rels-debug") << "[sets-rels] join term = " << join_terms[j] << std::endl;
               applyJoinRule(exp, join_terms[j]);
             }
           }
@@ -149,13 +151,12 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
               rel_terms[n.getKind()] = terms;
               d_terms_cache[r] = rel_terms;
             } else {
-              rel_terms = d_terms_cache[r];
               // No n's kind record is found
-              if( rel_terms.find(n.getKind()) == rel_terms.end() ) {
+              if( d_terms_cache[r].find(n.getKind()) == d_terms_cache[r].end() ) {
                 terms.push_back(n);
-                rel_terms[n.getKind()] = terms;
+                d_terms_cache[r][n.getKind()] = terms;
               } else {
-                rel_terms[n.getKind()].push_back(n);
+                d_terms_cache[r][n.getKind()].push_back(n);
               }
             }
           }