* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,

  DecisionEngine, and Theory.  These are triggered from the SmtEngine
  dtor before the other engines are deleted.  This is important
  because of potential issues with outstanding TNodes in Theory
  implementations (which fail if the destruction is done in the wrong
  order, in certain cases).

* Favor "FactQueueResetter" instead of clearAssertionQueues() for
  resetting facts queue in Theory implementations.

* Better theory-rewriting code.

* Minor cleanups.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index d6e1be9f2..6d949d6de 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -103,7 +103,7 @@ void TheoryUF::registerTerm(TNode n){
            "during backtracking");
   }else{
     //The attribute does not exist, so it is created and set
-    ecN = new (true) ECData(d_context, n);
+    ecN = new (true) ECData(getContext(), n);
     n.setAttribute(ECAttr(), ecN);
   }
 
@@ -134,7 +134,7 @@ void TheoryUF::registerTerm(TNode n){
         }
       }
 
-      ecChild->addPredecessor(n, d_context);
+      ecChild->addPredecessor(n, getContext());
     }
   }
   Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl;