diff options
author | Tim King <taking@cs.nyu.edu> | 2010-03-04 20:10:46 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-03-04 20:10:46 +0000 |
commit | 29cc307cdf2c42bebf4f5615874a864783f47fd0 (patch) | |
tree | bcc296eaef23abb9264d78adc3cfe08264f425ab /src/theory/uf/theory_uf.cpp | |
parent | 45b7c76aba6ac71726fb2bf46c45ad7ce6bc8c99 (diff) |
Committing a bug fix from Dejan. This resolves an issue with restoring ECData.
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 485f5f6d3..b4597c7c7 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -122,9 +122,9 @@ void TheoryUF::registerTerm(TNode n){ /* Because this can be called after nodes have been merged we may need * to be merged with other predecessors of the equivalence class. */ - for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->next ){ - if(equiv(n, Px->data)){ - Node pend = n.eqNode(Px->data); + for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ){ + if(equiv(n, Px->d_data)){ + Node pend = n.eqNode(Px->d_data); d_pending.push_back(pend); } } @@ -210,10 +210,10 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){ nslave->setFind(nmaster); - for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->next ){ - for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->next ){ - if(equiv(Px->data,Py->data)){ - Node pendingEq = (Px->data).eqNode(Py->data); + for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ){ + for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ){ + if(equiv(Px->d_data,Py->d_data)){ + Node pendingEq = (Px->d_data).eqNode(Py->d_data); d_pending.push_back(pendingEq); } } |