diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-18 12:39:24 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-18 12:39:24 -0600 |
| commit | eb940275067b14cf430348c67d85be2946c7aba3 (patch) | |
| tree | 64b27a41d5e85b2c109abd5f81044dd73334e6a2 | |
| parent | 3c42667a8f03d6dae5e419aca0d7711973b327b6 (diff) | |
Minor fix in relations.
| -rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index bd4ee5de0..a0a929ff9 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -1387,10 +1387,8 @@ int TheorySetsRels::EqcInfo::counter = 0; if(t1_ei != NULL && t2_ei != NULL) { if(!t1_ei->d_tc.get().isNull()) { NodeSet::const_iterator mem_it = t2_ei->d_mem.begin(); - while(mem_it != t2_ei->d_mem.end()) { - Assert( !t2_ei->d_tc.get().isNull() ); - addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*mem_it, t2_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*mem_it)).second); + addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*mem_it, t1_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*mem_it)).second); mem_it++; } } else if(!t2_ei->d_tc.get().isNull()) { @@ -1400,7 +1398,6 @@ int TheorySetsRels::EqcInfo::counter = 0; while(t1_mem_it != t1_ei->d_mem.end()) { NodeMap::const_iterator reason_it = t1_ei->d_mem_exp.find(*t1_mem_it); Assert(reason_it != t1_ei->d_mem_exp.end()); - Assert( !t1_ei->d_tc.get().isNull() ); addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*t1_mem_it, t1_ei->d_tc.get()), (*reason_it).second); t1_mem_it++; } @@ -1408,7 +1405,6 @@ int TheorySetsRels::EqcInfo::counter = 0; NodeSet::const_iterator t2_mem_it = t2_ei->d_mem.begin(); while(t2_mem_it != t2_ei->d_mem.end()) { - Assert( !t2_ei->d_tc.get().isNull() ); addTCMemAndSendInfer(t1_ei, NodeManager::currentNM()->mkNode(kind::MEMBER,*t2_mem_it, t2_ei->d_tc.get()), (*t2_ei->d_mem_exp.find(*t2_mem_it)).second); t2_mem_it++; } |