1 files changed, 9 insertions, 25 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1d623fdef..161c2eba6 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -73,10 +73,9 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
-SmtEngine::SmtEngine(ExprManager* em, Options* optr)
+SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
     : d_state(new SmtEngineState(*this)),
-      d_exprManager(em),
-      d_nodeManager(d_exprManager->getNodeManager()),
+      d_nodeManager(nm),
       d_absValues(new AbstractValues(d_nodeManager)),
       d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
       d_dumpm(new DumpManager(getUserContext())),
@@ -525,14 +524,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
   if (key == "all-statistics")
   {
     vector<SExpr> stats;
-    for (StatisticsRegistry::const_iterator i =
-             NodeManager::fromExprManager(d_exprManager)
-                 ->getStatisticsRegistry()
-                 ->begin();
-         i
-         != NodeManager::fromExprManager(d_exprManager)
-                ->getStatisticsRegistry()
-                ->end();
+    StatisticsRegistry* sr = d_nodeManager->getStatisticsRegistry();
+    for (StatisticsRegistry::const_iterator i = sr->begin(); i != sr->end();
          ++i)
     {
       vector<SExpr> v;
@@ -1637,7 +1630,6 @@ void SmtEngine::pop() {
 void SmtEngine::reset()
 {
   SmtScope smts(this);
-  ExprManager *em = d_exprManager;
   Trace("smt") << "SMT reset()" << endl;
   if(Dump.isOn("benchmark")) {
     getOutputManager().getPrinter().toStreamCmdReset(
@@ -1647,7 +1639,7 @@ void SmtEngine::reset()
   Options opts;
   opts.copyValues(d_originalOptions);
   this->~SmtEngine();
-  new (this) SmtEngine(em, &opts);
+  new (this) SmtEngine(d_nodeManager, &opts);
   // Restore data set after creation
   notifyStartParsing(filename);
 }
@@ -1713,10 +1705,7 @@ unsigned long SmtEngine::getResourceRemaining() const
   return d_resourceManager->getResourceRemaining();
 }
 
-NodeManager* SmtEngine::getNodeManager() const
-{
-  return d_exprManager->getNodeManager();
-}
+NodeManager* SmtEngine::getNodeManager() const { return d_nodeManager; }
 
 Statistics SmtEngine::getStatistics() const
 {
@@ -1733,20 +1722,15 @@ void SmtEngine::safeFlushStatistics(int fd) const {
 }
 
 void SmtEngine::setUserAttribute(const std::string& attr,
-                                 Expr expr,
-                                 const std::vector<Expr>& expr_values,
+                                 Node expr,
+                                 const std::vector<Node>& expr_values,
                                  const std::string& str_value)
 {
   SmtScope smts(this);
   finishInit();
-  std::vector<Node> node_values;
-  for (std::size_t i = 0, n = expr_values.size(); i < n; i++)
-  {
-    node_values.push_back( expr_values[i].getNode() );
-  }
   TheoryEngine* te = getTheoryEngine();
   Assert(te != nullptr);
-  te->setUserAttribute(attr, expr.getNode(), node_values, str_value);
+  te->setUserAttribute(attr, expr, expr_values, str_value);
 }
 
 void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)