TheoryUFWhite is passing. I fixed 2 errors. Unfortunately, I also changed a TNode...

diff --git a/src/theory/theory.h b/src/theory/theory.h
index efa67d6c48e0c5a5df44360e3c8e0fe87b8d5720..86badb9bd087c09eb14e4ee8a037aeaec99b84d3 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -324,8 +324,8 @@ Node TheoryImpl<T>::get() {
      * and the above registration of leaves, this should ensure that
      * all subterms in the entire tree were registered in
      * reverse-topological order. */
-    for(std::list<TNode>::reverse_iterator i = toReg.rend();
-        i != toReg.rbegin();
+    for(std::list<TNode>::reverse_iterator i = toReg.rbegin();
+        i != toReg.rend();
         ++i) {
 
       TNode n = *i;

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 0c0559bb0bee4a5705d5aa5416805704435e51f2..485f5f6d3c59eb8a2a015aa9607157a0f04d7bb6 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -124,7 +124,8 @@ void TheoryUF::registerTerm(TNode n){
        */
       for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->next ){
         if(equiv(n, Px->data)){
-          d_pending.push_back(n.eqNode(Px->data));
+          Node pend = n.eqNode(Px->data);
+          d_pending.push_back(pend);
         }
       }
 
@@ -223,7 +224,7 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
 
 void TheoryUF::merge(){
   while(d_currentPendingIdx < d_pending.size() ) {
-    TNode assertion = d_pending[d_currentPendingIdx];
+    Node assertion = d_pending[d_currentPendingIdx];
     d_currentPendingIdx = d_currentPendingIdx + 1;
 
     TNode x = assertion[0];