Fully decouple SmtEngine and the Expr layer (#5532)

This removes the remaining dependencies of SmtEngine on the Expr layer. It now takes a NodeManager instead of a ExprManager.

27 files changed, 49 insertions, 71 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 9b79b5c45..5eabcfe62 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3093,7 +3093,7 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
 Solver::Solver(Options* opts)
 {
   d_exprMgr.reset(new ExprManager);
-  d_smtEngine.reset(new SmtEngine(d_exprMgr.get(), opts));
+  d_smtEngine.reset(new SmtEngine(d_exprMgr->getNodeManager(), opts));
   d_smtEngine->setSolver(this);
   Options& o = d_smtEngine->getOptions();
   d_rng.reset(new Random(o[options::seed]));
diff --git a/src/expr/type.h b/src/expr/type.h
index 69a8363dc..0b923f027 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -33,7 +33,7 @@ class Expr;
 class TypeNode;
 struct CVC4_PUBLIC ExprManagerMapCollection;
 
-class CVC4_PUBLIC SmtEngine;
+class SmtEngine;
 
 class CVC4_PUBLIC Datatype;
 class Record;
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 154166eb7..fa3eb66c0 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1442,8 +1442,8 @@ void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm)
     {
       solver->getSmtEngine()->setUserAttribute(
           d_attr,
-          d_term.getExpr(),
-          api::termVectorToExprs(d_termValues),
+          d_term.getNode(),
+          api::termVectorToNodes(d_termValues),
           d_strValue);
     }
     d_commandStatus = CommandSuccess::instance();
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)
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 1c83fa61f..a55428b55 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -21,13 +21,12 @@
 
 #include <string>
 #include <vector>
+#include <map>
 
 #include "base/modal_exception.h"
 #include "context/cdhashmap_forward.h"
 #include "context/cdhashset_forward.h"
 #include "context/cdlist_forward.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
 #include "options/options.h"
 #include "smt/logic_exception.h"
 #include "smt/output_manager.h"
@@ -48,9 +47,10 @@ namespace CVC4 {
 template <bool ref_count> class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
+class TypeNode;
 struct NodeHashFunction;
 
-class SmtEngine;
+class NodeManager;
 class DecisionEngine;
 class TheoryEngine;
 class ProofManager;
@@ -58,6 +58,7 @@ class UnsatCore;
 class LogicRequest;
 class StatisticsRegistry;
 class Printer;
+class ResourceManager;
 
 /* -------------------------------------------------------------------------- */
 
@@ -147,7 +148,7 @@ class CVC4_PUBLIC SmtEngine
    * If provided, optr is a pointer to a set of options that should initialize the values
    * of the options object owned by this class.
    */
-  SmtEngine(ExprManager* em, Options* optr = nullptr);
+  SmtEngine(NodeManager* nm, Options* optr = nullptr);
   /** Destruct the SMT engine.  */
   ~SmtEngine();
 
@@ -691,7 +692,7 @@ class CVC4_PUBLIC SmtEngine
   /**
    * Completely reset the state of the solver, as though destroyed and
    * recreated.  The result is as if newly constructed (so it still
-   * retains the same options structure and ExprManager).
+   * retains the same options structure and NodeManager).
    */
   void reset();
 
@@ -785,9 +786,6 @@ class CVC4_PUBLIC SmtEngine
    */
   unsigned long getResourceRemaining() const;
 
-  /** Permit access to the underlying ExprManager. */
-  ExprManager* getExprManager() const { return d_exprManager; }
-
   /** Permit access to the underlying NodeManager. */
   NodeManager* getNodeManager() const;
 
@@ -806,8 +804,8 @@ class CVC4_PUBLIC SmtEngine
    * In SMT-LIBv2 this is done via the syntax (! expr :attr)
    */
   void 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);
 
   /** Get the options object (const and non-const versions) */
@@ -1013,9 +1011,7 @@ class CVC4_PUBLIC SmtEngine
    */
   std::unique_ptr<smt::SmtEngineState> d_state;
 
-  /** Our expression manager */
-  ExprManager* d_exprManager;
-  /** Our internal expression/node manager */
+  /** Our internal node manager */
   NodeManager* d_nodeManager;
   /** Abstract values */
   std::unique_ptr<smt::AbstractValues> d_absValues;
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index ed10e85ae..ee1ae198f 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -48,7 +48,7 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
   NodeManager* nm = NodeManager::currentNM();
   SmtEngine* smtCurr = smt::currentSmtEngine();
   // must copy the options
-  smte.reset(new SmtEngine(nm->toExprManager(), &smtCurr->getOptions()));
+  smte.reset(new SmtEngine(nm, &smtCurr->getOptions()));
   smte->setIsInternalSubsolver();
   smte->setLogic(smtCurr->getLogicInfo());
   // set the options
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index f1b782be2..de1795264 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -66,7 +66,7 @@ class AttributeWhite : public CxxTest::TestSuite {
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smtEngine = new SmtEngine(d_em);
+    d_smtEngine = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smtEngine);
     d_booleanType = new TypeNode(d_nm->booleanType());
   }
diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h
index 22d3f0d84..8ac17bbbd 100644
--- a/test/unit/expr/type_node_white.h
+++ b/test/unit/expr/type_node_white.h
@@ -42,7 +42,7 @@ class TypeNodeWhite : public CxxTest::TestSuite {
   {
     d_em = new ExprManager();
     d_nm = d_em->getNodeManager();
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new NodeManagerScope(d_nm);
   }
 
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h
index 0ff00a7d5..a0a708c5b 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.h
+++ b/test/unit/preprocessing/pass_bv_gauss_white.h
@@ -174,7 +174,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
 
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index ae79e1517..495097a79 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -131,9 +131,9 @@ class CnfStreamWhite : public CxxTest::TestSuite {
   void setUp() override
   {
     d_exprManager = new ExprManager();
-    d_smt = new SmtEngine(d_exprManager);
-    d_smt->d_logic.lock();
     d_nodeManager = NodeManager::fromExprManager(d_exprManager);
+    d_smt = new SmtEngine(d_nodeManager);
+    d_smt->d_logic.lock();
     d_scope = new SmtScope(d_smt);
 
     // Notice that this unit test uses the theory engine of a created SMT
diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
index 421987e3c..1f33d0fbf 100644
--- a/test/unit/theory/evaluator_white.h
+++ b/test/unit/theory/evaluator_white.h
@@ -50,7 +50,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
     d_em = new ExprManager;
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em, &opts);
+    d_smt = new SmtEngine(d_nm, &opts);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
   }
diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h
index 1215b4a31..09cb925a3 100644
--- a/test/unit/theory/sequences_rewriter_white.h
+++ b/test/unit/theory/sequences_rewriter_white.h
@@ -47,12 +47,11 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
     d_em = new ExprManager;
-    d_smt = new SmtEngine(d_em, &opts);
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm, &opts);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
     d_rewriter = new ExtendedRewriter(true);
-
-    d_nm = NodeManager::currentNM();
   }
 
   void tearDown() override
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index f0b3f18fe..3475b1dc8 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -101,7 +101,7 @@ public:
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_smt->setOption("incremental", CVC4::SExpr(false));
     d_ctxt = d_smt->getContext();
     d_uctxt = d_smt->getUserContext();
diff --git a/test/unit/theory/theory_bags_normal_form_white.h b/test/unit/theory/theory_bags_normal_form_white.h
index 4e19ba90e..72fc4284e 100644
--- a/test/unit/theory/theory_bags_normal_form_white.h
+++ b/test/unit/theory/theory_bags_normal_form_white.h
@@ -35,8 +35,8 @@ class BagsNormalFormWhite : public CxxTest::TestSuite
   void setUp() override
   {
     d_em.reset(new ExprManager());
-    d_smt.reset(new SmtEngine(d_em.get()));
     d_nm.reset(NodeManager::fromExprManager(d_em.get()));
+    d_smt.reset(new SmtEngine(d_nm.get()));
     d_smt->finishInit();
     d_rewriter.reset(new BagsRewriter(nullptr));
   }
diff --git a/test/unit/theory/theory_bags_rewriter_white.h b/test/unit/theory/theory_bags_rewriter_white.h
index e47e32784..a58e2cdad 100644
--- a/test/unit/theory/theory_bags_rewriter_white.h
+++ b/test/unit/theory/theory_bags_rewriter_white.h
@@ -34,8 +34,8 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite
   void setUp() override
   {
     d_em.reset(new ExprManager());
-    d_smt.reset(new SmtEngine(d_em.get()));
     d_nm.reset(NodeManager::fromExprManager(d_em.get()));
+    d_smt.reset(new SmtEngine(d_nm.get()));
     d_smt->finishInit();
     d_rewriter.reset(new BagsRewriter(nullptr));
   }
diff --git a/test/unit/theory/theory_bags_type_rules_white.h b/test/unit/theory/theory_bags_type_rules_white.h
index e454dfa28..8d1db858d 100644
--- a/test/unit/theory/theory_bags_type_rules_white.h
+++ b/test/unit/theory/theory_bags_type_rules_white.h
@@ -34,8 +34,8 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite
   void setUp() override
   {
     d_em.reset(new ExprManager());
-    d_smt.reset(new SmtEngine(d_em.get()));
     d_nm.reset(NodeManager::fromExprManager(d_em.get()));
+    d_smt.reset(new SmtEngine(d_nm.get()));
     d_smt->finishInit();
   }
 
diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h
index fae90918a..738a51831 100644
--- a/test/unit/theory/theory_bv_rewriter_white.h
+++ b/test/unit/theory/theory_bv_rewriter_white.h
@@ -41,11 +41,10 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
     d_em = new ExprManager;
-    d_smt = new SmtEngine(d_em, &opts);
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm, &opts);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
-
-    d_nm = NodeManager::currentNM();
   }
 
   void tearDown() override
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index bfde7866e..f568dc779 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -54,7 +54,7 @@ public:
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smt);
   }
 
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 8a99946e5..97da7eb8b 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -192,8 +192,8 @@ public:
 
   void setUp() override {
     d_em = new ExprManager();
-    d_smt = new SmtEngine(d_em);
     d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smt);
 
     d_ctxt = d_smt->getContext();
diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
index f2c5f0e1d..e19459f15 100644
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
@@ -63,7 +63,7 @@ void BvInstantiatorWhite::setUp()
 {
   d_em = new ExprManager();
   d_nm = NodeManager::fromExprManager(d_em);
-  d_smt = new SmtEngine(d_em);
+  d_smt = new SmtEngine(d_nm);
   d_scope = new SmtScope(d_smt);
   d_smt->finishInit();
 }
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
index bb44656bc..ac25f60a9 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
@@ -222,7 +222,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_smt->setOption("cegqi-full", CVC4::SExpr(true));
     d_smt->setOption("produce-models", CVC4::SExpr(true));
     d_scope = new SmtScope(d_smt);
diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
index 965e59267..1b5ba1dcb 100644
--- a/test/unit/theory/theory_sets_type_enumerator_white.h
+++ b/test/unit/theory/theory_sets_type_enumerator_white.h
@@ -36,8 +36,8 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
   void setUp() override
   {
     d_em = new ExprManager();
-    d_smt = new SmtEngine(d_em);
     d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
   }
diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h
index 66c8dc123..00b012745 100644
--- a/test/unit/theory/theory_sets_type_rules_white.h
+++ b/test/unit/theory/theory_sets_type_rules_white.h
@@ -28,8 +28,8 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite
   {
     d_slv.reset(new Solver());
     d_em.reset(new ExprManager());
-    d_smt.reset(new SmtEngine(d_em.get()));
     d_nm.reset(NodeManager::fromExprManager(d_em.get()));
+    d_smt.reset(new SmtEngine(d_nm.get()));
     d_smt->finishInit();
   }
 
diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h
index 4135adb0c..dd70dd5b9 100644
--- a/test/unit/theory/theory_strings_skolem_cache_black.h
+++ b/test/unit/theory/theory_strings_skolem_cache_black.h
@@ -35,13 +35,13 @@ class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite
   void setUp() override
   {
     d_em.reset(new ExprManager());
-    d_smt.reset(new SmtEngine(d_em.get()));
+    d_nm = NodeManager::fromExprManager(d_em.get());
+    d_smt.reset(new SmtEngine(d_nm));
     d_scope.reset(new SmtScope(d_smt.get()));
     // Ensure that the SMT engine is fully initialized (required for the
     // rewriter)
     d_smt->push();
 
-    d_nm = NodeManager::fromExprManager(d_em.get());
   }
 
   void tearDown() override {}
diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h
index 69143a69c..ce432d385 100644
--- a/test/unit/theory/theory_strings_word_white.h
+++ b/test/unit/theory/theory_strings_word_white.h
@@ -38,10 +38,10 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
     d_em = new ExprManager;
-    d_smt = new SmtEngine(d_em, &opts);
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm, &opts);
     d_scope = new SmtScope(d_smt);
 
-    d_nm = NodeManager::currentNM();
   }
 
   void tearDown() override
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 552aeb3c6..f69830fd8 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -175,7 +175,7 @@ class TheoryBlack : public CxxTest::TestSuite {
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_ctxt = d_smt->getContext();
     d_uctxt = d_smt->getUserContext();
     d_scope = new SmtScope(d_smt);
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index ea5a38913..24bf9922e 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -42,8 +42,8 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
   void setUp() override
   {
     d_em = new ExprManager();
-    d_smt = new SmtEngine(d_em);
     d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
   }