From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 17 Sep 2021 23:14:42 +0000 (-0700)
Subject: Use a single `NodeManager` per thread (#7204)
X-Git-Tag: cvc5-1.0.0~1199
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4209fb71c97c06833ef320ad9c73590546c16fa2;p=cvc5.git

Use a single `NodeManager` per thread (#7204)

This changes cvc5 to use a single `NodeManager` per thread (using
`thread_local`). We have decided that this is more convenient because
nodes between solvers in the same thread could be exchanged and that
there isn't really an advantage of having multiple `NodeManager`s per
thread.

One wrinkle of this change is that `NodeManager::init()` must be called
explicitly before the `NodeManager` can be used. This code can currently
not be moved to the constructor of `NodeManager` because the code
indirectly calls `NodeManager::currentNM()`, which leads to a loop
because the `NodeManager` is created in `NodeManager::currentNM()`.
Further refactoring is required to get rid of this restriction.
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 6aa556ed8..2a98ee36a 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -994,9 +994,6 @@ Sort::~Sort()
 {
   if (d_solver != nullptr)
   {
-    // Ensure that the correct node manager is in scope when the node is
-    // destroyed.
-    NodeManagerScope scope(d_solver->getNodeManager());
     d_type.reset();
   }
 }
@@ -1354,7 +1351,6 @@ bool Sort::isComparableTo(const Sort& s) const
 
 Datatype Sort::getDatatype() const
 {
-  NodeManagerScope scope(d_solver->getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK(isDatatype()) << "Expected datatype sort.";
@@ -1366,7 +1362,6 @@ Datatype Sort::getDatatype() const
 
 Sort Sort::instantiate(const std::vector<Sort>& params) const
 {
-  NodeManagerScope scope(d_solver->getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK_SORTS(params);
@@ -1386,7 +1381,6 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
 
 Sort Sort::substitute(const Sort& sort, const Sort& replacement) const
 {
-  NodeManagerScope scope(d_solver->getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK_SORT(sort);
@@ -1402,7 +1396,6 @@ Sort Sort::substitute(const Sort& sort, const Sort& replacement) const
 Sort Sort::substitute(const std::vector<Sort>& sorts,
                       const std::vector<Sort>& replacements) const
 {
-  NodeManagerScope scope(d_solver->getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK_SORTS(sorts);
@@ -1427,7 +1420,6 @@ std::string Sort::toString() const
   //////// all checks before this line
   if (d_solver != nullptr)
   {
-    NodeManagerScope scope(d_solver->getNodeManager());
     return d_type->toString();
   }
   return d_type->toString();
@@ -1811,7 +1803,6 @@ Op::~Op()
   {
     // Ensure that the correct node manager is in scope when the type node is
     // destroyed.
-    NodeManagerScope scope(d_solver->getNodeManager());
     d_node.reset();
   }
 }
@@ -2267,7 +2258,6 @@ std::string Op::toString() const
         << "Expecting a non-null internal expression";
     if (d_solver != nullptr)
     {
-      NodeManagerScope scope(d_solver->getNodeManager());
       return d_node->toString();
     }
     return d_node->toString();
@@ -2303,8 +2293,6 @@ Term::Term() : d_solver(nullptr), d_node(new cvc5::Node()) {}
 
 Term::Term(const Solver* slv, const cvc5::Node& n) : d_solver(slv)
 {
-  // Ensure that we create the node in the correct node manager.
-  NodeManagerScope scope(d_solver->getNodeManager());
   d_node.reset(new cvc5::Node(n));
 }
 
@@ -2312,9 +2300,6 @@ Term::~Term()
 {
   if (d_solver != nullptr)
   {
-    // Ensure that the correct node manager is in scope when the node is
-    // destroyed.
-    NodeManagerScope scope(d_solver->getNodeManager());
     d_node.reset();
   }
 }
@@ -2445,7 +2430,6 @@ Sort Term::getSort() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
-  NodeManagerScope scope(d_solver->getNodeManager());
   //////// all checks before this line
   return Sort(d_solver, d_node->getType());
   ////////
@@ -2635,7 +2619,6 @@ std::string Term::toString() const
   //////// all checks before this line
   if (d_solver != nullptr)
   {
-    NodeManagerScope scope(d_solver->getNodeManager());
     return d_node->toString();
   }
   return d_node->toString();
@@ -3468,8 +3451,6 @@ DatatypeConstructorDecl::~DatatypeConstructorDecl()
 {
   if (d_ctor != nullptr)
   {
-    // ensure proper node manager is in scope
-    NodeManagerScope scope(d_solver->getNodeManager());
     d_ctor.reset();
   }
 }
@@ -3477,7 +3458,6 @@ DatatypeConstructorDecl::~DatatypeConstructorDecl()
 void DatatypeConstructorDecl::addSelector(const std::string& name,
                                           const Sort& sort)
 {
-  NodeManagerScope scope(d_solver->getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK_SORT(sort);
@@ -3491,7 +3471,6 @@ void DatatypeConstructorDecl::addSelector(const std::string& name,
 
 void DatatypeConstructorDecl::addSelectorSelf(const std::string& name)
 {
-  NodeManagerScope scope(d_solver->getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   //////// all checks before this line
@@ -3574,15 +3553,12 @@ DatatypeDecl::~DatatypeDecl()
 {
   if (d_dtype != nullptr)
   {
-    // ensure proper node manager is in scope
-    NodeManagerScope scope(d_solver->getNodeManager());
     d_dtype.reset();
   }
 }
 
 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
 {
-  NodeManagerScope scope(d_solver->getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_ARG_CHECK_NOT_NULL(ctor);
@@ -3667,8 +3643,6 @@ DatatypeSelector::~DatatypeSelector()
 {
   if (d_stor != nullptr)
   {
-    // ensure proper node manager is in scope
-    NodeManagerScope scope(d_solver->getNodeManager());
     d_stor.reset();
   }
 }
@@ -3758,8 +3732,6 @@ DatatypeConstructor::~DatatypeConstructor()
 {
   if (d_ctor != nullptr)
   {
-    // ensure proper node manager is in scope
-    NodeManagerScope scope(d_solver->getNodeManager());
     d_ctor.reset();
   }
 }
@@ -3787,7 +3759,6 @@ Term DatatypeConstructor::getConstructorTerm() const
 Term DatatypeConstructor::getSpecializedConstructorTerm(
     const Sort& retSort) const
 {
-  NodeManagerScope scope(d_solver->getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   CVC5_API_CHECK(d_ctor->isResolved())
@@ -4021,8 +3992,6 @@ Datatype::~Datatype()
 {
   if (d_dtype != nullptr)
   {
-    // ensure proper node manager is in scope
-    NodeManagerScope scope(d_solver->getNodeManager());
     d_dtype.reset();
   }
 }
@@ -4974,9 +4943,10 @@ std::ostream& operator<<(std::ostream& out, const Statistics& stats)
 
 Solver::Solver(std::unique_ptr<Options>&& original)
 {
-  d_nodeMgr.reset(new NodeManager());
+  d_nodeMgr = NodeManager::currentNM();
+  d_nodeMgr->init();
   d_originalOptions = std::move(original);
-  d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get()));
+  d_smtEngine.reset(new SmtEngine(d_nodeMgr, d_originalOptions.get()));
   d_smtEngine->setSolver(this);
   d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed));
   resetStatistics();
@@ -4989,7 +4959,7 @@ Solver::~Solver() {}
 /* Helpers and private functions                                              */
 /* -------------------------------------------------------------------------- */
 
-NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr.get(); }
+NodeManager* Solver::getNodeManager(void) const { return d_nodeMgr; }
 
 void Solver::increment_term_stats(Kind kind) const
 {
@@ -5433,7 +5403,6 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
 
 Sort Solver::getNullSort(void) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Sort(this, TypeNode());
@@ -5443,7 +5412,6 @@ Sort Solver::getNullSort(void) const
 
 Sort Solver::getBooleanSort(void) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Sort(this, getNodeManager()->booleanType());
@@ -5453,7 +5421,6 @@ Sort Solver::getBooleanSort(void) const
 
 Sort Solver::getIntegerSort(void) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Sort(this, getNodeManager()->integerType());
@@ -5463,7 +5430,6 @@ Sort Solver::getIntegerSort(void) const
 
 Sort Solver::getRealSort(void) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Sort(this, getNodeManager()->realType());
@@ -5473,7 +5439,6 @@ Sort Solver::getRealSort(void) const
 
 Sort Solver::getRegExpSort(void) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Sort(this, getNodeManager()->regExpType());
@@ -5483,7 +5448,6 @@ Sort Solver::getRegExpSort(void) const
 
 Sort Solver::getStringSort(void) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Sort(this, getNodeManager()->stringType());
@@ -5493,7 +5457,6 @@ Sort Solver::getStringSort(void) const
 
 Sort Solver::getRoundingModeSort(void) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Sort(this, getNodeManager()->roundingModeType());
@@ -5505,7 +5468,6 @@ Sort Solver::getRoundingModeSort(void) const
 
 Sort Solver::mkArraySort(const Sort& indexSort, const Sort& elemSort) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(indexSort);
   CVC5_API_SOLVER_CHECK_SORT(elemSort);
@@ -5518,7 +5480,6 @@ Sort Solver::mkArraySort(const Sort& indexSort, const Sort& elemSort) const
 
 Sort Solver::mkBitVectorSort(uint32_t size) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0";
   //////// all checks before this line
@@ -5529,7 +5490,6 @@ Sort Solver::mkBitVectorSort(uint32_t size) const
 
 Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0";
   CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
@@ -5541,7 +5501,6 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
 
 Sort Solver::mkDatatypeSort(const DatatypeDecl& dtypedecl) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_DTDECL(dtypedecl);
   //////// all checks before this line
@@ -5553,7 +5512,6 @@ Sort Solver::mkDatatypeSort(const DatatypeDecl& dtypedecl) const
 std::vector<Sort> Solver::mkDatatypeSorts(
     const std::vector<DatatypeDecl>& dtypedecls) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls);
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
@@ -5566,7 +5524,6 @@ std::vector<Sort> Solver::mkDatatypeSorts(
     const std::vector<DatatypeDecl>& dtypedecls,
     const std::set<Sort>& unresolvedSorts) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_DTDECLS(dtypedecls);
   CVC5_API_SOLVER_CHECK_SORTS(unresolvedSorts);
@@ -5578,7 +5535,6 @@ std::vector<Sort> Solver::mkDatatypeSorts(
 
 Sort Solver::mkFunctionSort(const Sort& domain, const Sort& codomain) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_DOMAIN_SORT(domain);
   CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(codomain);
@@ -5592,7 +5548,6 @@ Sort Solver::mkFunctionSort(const Sort& domain, const Sort& codomain) const
 Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts,
                             const Sort& codomain) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts)
       << "at least one parameter sort for function sort";
@@ -5608,7 +5563,6 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts,
 
 Sort Solver::mkParamSort(const std::string& symbol) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Sort(
@@ -5620,7 +5574,6 @@ Sort Solver::mkParamSort(const std::string& symbol) const
 
 Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts)
       << "at least one parameter sort for predicate sort";
@@ -5636,7 +5589,6 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
 Sort Solver::mkRecordSort(
     const std::vector<std::pair<std::string, Sort>>& fields) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   std::vector<std::pair<std::string, TypeNode>> f;
   for (size_t i = 0, size = fields.size(); i < size; ++i)
@@ -5657,7 +5609,6 @@ Sort Solver::mkRecordSort(
 
 Sort Solver::mkSetSort(const Sort& elemSort) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(elemSort);
   //////// all checks before this line
@@ -5668,7 +5619,6 @@ Sort Solver::mkSetSort(const Sort& elemSort) const
 
 Sort Solver::mkBagSort(const Sort& elemSort) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(elemSort);
   //////// all checks before this line
@@ -5679,7 +5629,6 @@ Sort Solver::mkBagSort(const Sort& elemSort) const
 
 Sort Solver::mkSequenceSort(const Sort& elemSort) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(elemSort);
   //////// all checks before this line
@@ -5690,7 +5639,6 @@ Sort Solver::mkSequenceSort(const Sort& elemSort) const
 
 Sort Solver::mkUninterpretedSort(const std::string& symbol) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Sort(this, getNodeManager()->mkSort(symbol));
@@ -5701,7 +5649,6 @@ Sort Solver::mkUninterpretedSort(const std::string& symbol) const
 Sort Solver::mkSortConstructorSort(const std::string& symbol,
                                    size_t arity) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0";
   //////// all checks before this line
@@ -5712,7 +5659,6 @@ Sort Solver::mkSortConstructorSort(const std::string& symbol,
 
 Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORTS_NOT_FUNCTION_LIKE(sorts);
   //////// all checks before this line
@@ -5726,7 +5672,6 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
 
 Term Solver::mkTrue(void) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Term(this, d_nodeMgr->mkConst<bool>(true));
@@ -5736,7 +5681,6 @@ Term Solver::mkTrue(void) const
 
 Term Solver::mkFalse(void) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Term(this, d_nodeMgr->mkConst<bool>(false));
@@ -5746,7 +5690,6 @@ Term Solver::mkFalse(void) const
 
 Term Solver::mkBoolean(bool val) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return Term(this, d_nodeMgr->mkConst<bool>(val));
@@ -5756,7 +5699,6 @@ Term Solver::mkBoolean(bool val) const
 
 Term Solver::mkPi() const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   Node res =
@@ -5769,7 +5711,6 @@ Term Solver::mkPi() const
 
 Term Solver::mkInteger(const std::string& s) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_CHECK_EXPECTED(isValidInteger(s), s) << " an integer ";
   Term integer = mkRealFromStrHelper(s);
@@ -5783,7 +5724,6 @@ Term Solver::mkInteger(const std::string& s) const
 
 Term Solver::mkInteger(int64_t val) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   Term integer = mkValHelper<cvc5::Rational>(cvc5::Rational(val));
@@ -5795,7 +5735,6 @@ Term Solver::mkInteger(int64_t val) const
 
 Term Solver::mkReal(const std::string& s) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
    * throws an std::invalid_argument exception. For consistency, we treat it
@@ -5811,7 +5750,6 @@ Term Solver::mkReal(const std::string& s) const
 
 Term Solver::mkReal(int64_t val) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   Term rational = mkValHelper<cvc5::Rational>(cvc5::Rational(val));
@@ -5822,7 +5760,6 @@ Term Solver::mkReal(int64_t val) const
 
 Term Solver::mkReal(int64_t num, int64_t den) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   Term rational = mkValHelper<cvc5::Rational>(cvc5::Rational(num, den));
@@ -5833,7 +5770,6 @@ Term Solver::mkReal(int64_t num, int64_t den) const
 
 Term Solver::mkRegexpEmpty() const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   Node res =
@@ -5846,7 +5782,6 @@ Term Solver::mkRegexpEmpty() const
 
 Term Solver::mkRegexpSigma() const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   Node res =
@@ -5859,7 +5794,6 @@ Term Solver::mkRegexpSigma() const
 
 Term Solver::mkEmptySet(const Sort& sort) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_CHECK_EXPECTED(sort.isNull() || sort.isSet(), sort)
       << "null sort or set sort";
@@ -5873,7 +5807,6 @@ Term Solver::mkEmptySet(const Sort& sort) const
 
 Term Solver::mkEmptyBag(const Sort& sort) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_CHECK_EXPECTED(sort.isNull() || sort.isBag(), sort)
       << "null sort or bag sort";
@@ -5887,7 +5820,6 @@ Term Solver::mkEmptyBag(const Sort& sort) const
 
 Term Solver::mkSepNil(const Sort& sort) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
   //////// all checks before this line
@@ -5901,7 +5833,6 @@ Term Solver::mkSepNil(const Sort& sort) const
 
 Term Solver::mkString(const std::string& s, bool useEscSequences) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return mkValHelper<cvc5::String>(cvc5::String(s, useEscSequences));
@@ -5911,7 +5842,6 @@ Term Solver::mkString(const std::string& s, bool useEscSequences) const
 
 Term Solver::mkString(const std::wstring& s) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return mkValHelper<cvc5::String>(cvc5::String(s));
@@ -5921,7 +5851,6 @@ Term Solver::mkString(const std::wstring& s) const
 
 Term Solver::mkEmptySequence(const Sort& sort) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
   //////// all checks before this line
@@ -5934,7 +5863,6 @@ Term Solver::mkEmptySequence(const Sort& sort) const
 
 Term Solver::mkUniverseSet(const Sort& sort) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
   //////// all checks before this line
@@ -5950,7 +5878,6 @@ Term Solver::mkUniverseSet(const Sort& sort) const
 
 Term Solver::mkBitVector(uint32_t size, uint64_t val) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return mkBVFromIntHelper(size, val);
@@ -5962,7 +5889,6 @@ Term Solver::mkBitVector(uint32_t size,
                          const std::string& s,
                          uint32_t base) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return mkBVFromStrHelper(size, s, base);
@@ -5972,7 +5898,6 @@ Term Solver::mkBitVector(uint32_t size,
 
 Term Solver::mkConstArray(const Sort& sort, const Term& val) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
   CVC5_API_SOLVER_CHECK_TERM(val);
@@ -5997,7 +5922,6 @@ Term Solver::mkConstArray(const Sort& sort, const Term& val) const
 
 Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
@@ -6008,7 +5932,6 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
 
 Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
@@ -6019,7 +5942,6 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
 
 Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
@@ -6030,7 +5952,6 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
 
 Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
@@ -6041,7 +5962,6 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
 
 Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
@@ -6052,7 +5972,6 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
 
 Term Solver::mkRoundingMode(RoundingMode rm) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return mkValHelper<cvc5::RoundingMode>(s_rmodes.at(rm));
@@ -6062,7 +5981,6 @@ Term Solver::mkRoundingMode(RoundingMode rm) const
 
 Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
   //////// all checks before this line
@@ -6074,7 +5992,6 @@ Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const
 
 Term Solver::mkAbstractValue(const std::string& index) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string";
 
@@ -6091,7 +6008,6 @@ Term Solver::mkAbstractValue(const std::string& index) const
 
 Term Solver::mkAbstractValue(uint64_t index) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0";
   //////// all checks before this line
@@ -6105,7 +6021,6 @@ Term Solver::mkAbstractValue(uint64_t index) const
 
 Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(val);
   CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0";
@@ -6128,7 +6043,6 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
 
 Term Solver::mkConst(const Sort& sort, const std::string& symbol) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
   //////// all checks before this line
@@ -6142,7 +6056,6 @@ Term Solver::mkConst(const Sort& sort, const std::string& symbol) const
 
 Term Solver::mkConst(const Sort& sort) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
   //////// all checks before this line
@@ -6159,7 +6072,6 @@ Term Solver::mkConst(const Sort& sort) const
 
 Term Solver::mkVar(const Sort& sort, const std::string& symbol) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
   //////// all checks before this line
@@ -6178,7 +6090,6 @@ Term Solver::mkVar(const Sort& sort, const std::string& symbol) const
 DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl(
     const std::string& name)
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return DatatypeConstructorDecl(this, name);
@@ -6191,7 +6102,6 @@ DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl(
 
 DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype)
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   return DatatypeDecl(this, name, isCoDatatype);
@@ -6203,7 +6113,6 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name,
                                     Sort param,
                                     bool isCoDatatype)
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(param);
   //////// all checks before this line
@@ -6216,7 +6125,6 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name,
                                     const std::vector<Sort>& params,
                                     bool isCoDatatype)
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORTS(params);
   //////// all checks before this line
@@ -6230,7 +6138,6 @@ DatatypeDecl Solver::mkDatatypeDecl(const std::string& name,
 
 Term Solver::mkTerm(Kind kind) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_KIND_CHECK(kind);
   //////// all checks before this line
@@ -6241,7 +6148,6 @@ Term Solver::mkTerm(Kind kind) const
 
 Term Solver::mkTerm(Kind kind, const Term& child) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_KIND_CHECK(kind);
   CVC5_API_SOLVER_CHECK_TERM(child);
@@ -6253,7 +6159,6 @@ Term Solver::mkTerm(Kind kind, const Term& child) const
 
 Term Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_KIND_CHECK(kind);
   CVC5_API_SOLVER_CHECK_TERM(child1);
@@ -6269,7 +6174,6 @@ Term Solver::mkTerm(Kind kind,
                     const Term& child2,
                     const Term& child3) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_KIND_CHECK(kind);
   CVC5_API_SOLVER_CHECK_TERM(child1);
@@ -6284,7 +6188,6 @@ Term Solver::mkTerm(Kind kind,
 
 Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_KIND_CHECK(kind);
   CVC5_API_SOLVER_CHECK_TERMS(children);
@@ -6296,7 +6199,6 @@ Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
 
 Term Solver::mkTerm(const Op& op) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_OP(op);
   checkMkTerm(op.d_kind, 0);
@@ -6318,7 +6220,6 @@ Term Solver::mkTerm(const Op& op) const
 
 Term Solver::mkTerm(const Op& op, const Term& child) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_OP(op);
   CVC5_API_SOLVER_CHECK_TERM(child);
@@ -6330,7 +6231,6 @@ Term Solver::mkTerm(const Op& op, const Term& child) const
 
 Term Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_OP(op);
   CVC5_API_SOLVER_CHECK_TERM(child1);
@@ -6346,7 +6246,6 @@ Term Solver::mkTerm(const Op& op,
                     const Term& child2,
                     const Term& child3) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_OP(op);
   CVC5_API_SOLVER_CHECK_TERM(child1);
@@ -6360,7 +6259,6 @@ Term Solver::mkTerm(const Op& op,
 
 Term Solver::mkTerm(const Op& op, const std::vector<Term>& children) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_OP(op);
   CVC5_API_SOLVER_CHECK_TERMS(children);
@@ -6373,7 +6271,6 @@ Term Solver::mkTerm(const Op& op, const std::vector<Term>& children) const
 Term Solver::mkTuple(const std::vector<Sort>& sorts,
                      const std::vector<Term>& terms) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(sorts.size() == terms.size())
       << "Expected the same number of sorts and elements";
@@ -6630,7 +6527,6 @@ Op Solver::mkOp(Kind kind, const std::vector<uint32_t>& args) const
 
 Term Solver::simplify(const Term& term)
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(term);
   //////// all checks before this line
@@ -6641,7 +6537,6 @@ Term Solver::simplify(const Term& term)
 
 Result Solver::checkEntailed(const Term& term) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
                  || d_smtEngine->getOptions().base.incrementalSolving)
@@ -6657,7 +6552,6 @@ Result Solver::checkEntailed(const Term& term) const
 Result Solver::checkEntailed(const std::vector<Term>& terms) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
                  || d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
@@ -6686,7 +6580,6 @@ void Solver::assertFormula(const Term& term) const
 Result Solver::checkSat(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
                  || d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
@@ -6700,7 +6593,6 @@ Result Solver::checkSat(void) const
 Result Solver::checkSatAssuming(const Term& assumption) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
                  || d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
@@ -6715,7 +6607,6 @@ Result Solver::checkSatAssuming(const Term& assumption) const
 Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
                  || d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
@@ -6857,7 +6748,6 @@ Term Solver::defineFunRec(const std::string& symbol,
                           const Term& term,
                           bool global) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
 
   CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
@@ -6902,7 +6792,6 @@ Term Solver::defineFunRec(const Term& fun,
                           const Term& term,
                           bool global) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
 
   CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
@@ -6944,7 +6833,6 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
                            const std::vector<Term>& terms,
                            bool global) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
 
   CVC5_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
@@ -7245,7 +7133,6 @@ DriverOptions Solver::getDriverOptions() const { return DriverOptions(*this); }
 std::vector<Term> Solver::getUnsatAssumptions(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot get unsat assumptions unless incremental solving is enabled "
          "(try --incremental)";
@@ -7273,7 +7160,6 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
 std::vector<Term> Solver::getUnsatCore(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatCores)
       << "Cannot get unsat core unless explicitly enabled "
          "(try --produce-unsat-cores)";
@@ -7297,7 +7183,6 @@ std::vector<Term> Solver::getUnsatCore(void) const
 std::map<Term, Term> Solver::getDifficulty() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT
                              || d_smtEngine->getSmtMode() == SmtMode::SAT
                              || d_smtEngine->getSmtMode()
@@ -7319,7 +7204,6 @@ std::map<Term, Term> Solver::getDifficulty() const
 std::string Solver::getProof(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceProofs)
       << "Cannot get proof explicitly enabled (try --produce-proofs)";
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
@@ -7341,7 +7225,6 @@ Term Solver::getValue(const Term& term) const
 std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
@@ -7364,7 +7247,6 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
 std::vector<Term> Solver::getModelDomainElements(const Sort& s) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot get domain elements unless model generation is enabled "
          "(try --produce-models)";
@@ -7390,7 +7272,6 @@ std::vector<Term> Solver::getModelDomainElements(const Sort& s) const
 bool Solver::isModelCoreSymbol(const Term& v) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot check if model core symbol unless model generation is enabled "
          "(try --produce-models)";
@@ -7410,7 +7291,6 @@ std::string Solver::getModel(const std::vector<Sort>& sorts,
                              const std::vector<Term>& vars) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot get model unless model generation is enabled "
          "(try --produce-models)";
@@ -7438,7 +7318,6 @@ std::string Solver::getModel(const std::vector<Sort>& sorts,
 
 Term Solver::getQuantifierElimination(const Term& q) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(q);
   //////// all checks before this line
@@ -7450,7 +7329,6 @@ Term Solver::getQuantifierElimination(const Term& q) const
 
 Term Solver::getQuantifierEliminationDisjunct(const Term& q) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(q);
   //////// all checks before this line
@@ -7478,7 +7356,6 @@ void Solver::declareSeparationHeap(const Sort& locSort,
 
 Term Solver::getSeparationHeap() const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(
       d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
@@ -7497,7 +7374,6 @@ Term Solver::getSeparationHeap() const
 
 Term Solver::getSeparationNilTerm() const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(
       d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
@@ -7518,7 +7394,6 @@ Term Solver::declarePool(const std::string& symbol,
                          const Sort& sort,
                          const std::vector<Term>& initValue) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_SORT(sort);
   CVC5_API_SOLVER_CHECK_TERMS(initValue);
@@ -7534,7 +7409,6 @@ Term Solver::declarePool(const std::string& symbol,
 
 void Solver::pop(uint32_t nscopes) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot pop when not solving incrementally (use --incremental)";
@@ -7551,7 +7425,6 @@ void Solver::pop(uint32_t nscopes) const
 
 bool Solver::getInterpolant(const Term& conj, Term& output) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
   //////// all checks before this line
@@ -7570,7 +7443,6 @@ bool Solver::getInterpolant(const Term& conj,
                             Grammar& grammar,
                             Term& output) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
   //////// all checks before this line
@@ -7588,7 +7460,6 @@ bool Solver::getInterpolant(const Term& conj,
 
 bool Solver::getAbduct(const Term& conj, Term& output) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
   //////// all checks before this line
@@ -7605,7 +7476,6 @@ bool Solver::getAbduct(const Term& conj, Term& output) const
 
 bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
   //////// all checks before this line
@@ -7623,7 +7493,6 @@ bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const
 
 void Solver::blockModel() const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot get value unless model generation is enabled "
@@ -7638,7 +7507,6 @@ void Solver::blockModel() const
 
 void Solver::blockModelValues(const std::vector<Term>& terms) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot get value unless model generation is enabled "
@@ -7656,7 +7524,6 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
 
 void Solver::printInstantiations(std::ostream& out) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   d_smtEngine->printInstantiations(out);
@@ -7666,7 +7533,6 @@ void Solver::printInstantiations(std::ostream& out) const
 
 void Solver::push(uint32_t nscopes) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(d_smtEngine->getOptions().base.incrementalSolving)
       << "Cannot push when not solving incrementally (use --incremental)";
@@ -7834,7 +7700,6 @@ Term Solver::synthInv(const std::string& symbol,
 
 void Solver::addSygusConstraint(const Term& term) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(term);
   CVC5_API_ARG_CHECK_EXPECTED(
@@ -7848,7 +7713,6 @@ void Solver::addSygusConstraint(const Term& term) const
 
 void Solver::addSygusAssume(const Term& term) const
 {
-  NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(term);
   CVC5_API_ARG_CHECK_EXPECTED(
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 4f1c60814..248bb8bda 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4491,7 +4491,7 @@ class CVC5_EXPORT Solver
   /** Keep a copy of the original option settings (for resets). */
   std::unique_ptr<Options> d_originalOptions;
   /** The node manager of this solver. */
-  std::unique_ptr<NodeManager> d_nodeMgr;
+  NodeManager* d_nodeMgr;
   /** The statistics collected on the Api level. */
   std::unique_ptr<APIStatistics> d_stats;
   /** The SMT engine of this solver. */
diff --git a/src/expr/node.h b/src/expr/node.h
index 1ce915472..13885a0f2 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1007,10 +1007,6 @@ template <bool ref_count>
 template <class AttrKind>
 inline typename AttrKind::value_type NodeTemplate<ref_count>::
 getAttribute(const AttrKind&) const {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
-
   assertTNodeNotExpired();
 
   return NodeManager::currentNM()->getAttribute(*this, AttrKind());
@@ -1020,10 +1016,6 @@ template <bool ref_count>
 template <class AttrKind>
 inline bool NodeTemplate<ref_count>::
 hasAttribute(const AttrKind&) const {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
-
   assertTNodeNotExpired();
 
   return NodeManager::currentNM()->hasAttribute(*this, AttrKind());
@@ -1033,10 +1025,6 @@ template <bool ref_count>
 template <class AttrKind>
 inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&,
                                                   typename AttrKind::value_type& ret) const {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
-
   assertTNodeNotExpired();
 
   return NodeManager::currentNM()->getAttribute(*this, AttrKind(), ret);
@@ -1046,10 +1034,6 @@ template <bool ref_count>
 template <class AttrKind>
 inline void NodeTemplate<ref_count>::
 setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
-
   assertTNodeNotExpired();
 
   NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
@@ -1246,10 +1230,6 @@ NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
 template <bool ref_count>
 NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const
 {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
-
   assertTNodeNotExpired();
 
   kind::MetaKind mk = getMetaKind();
@@ -1276,10 +1256,6 @@ inline bool NodeTemplate<ref_count>::hasOperator() const {
 template <bool ref_count>
 TypeNode NodeTemplate<ref_count>::getType(bool check) const
 {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
-
   assertTNodeNotExpired();
 
   return NodeManager::currentNM()->getType(*this, check);
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index fe7d75ca3..1222f3c9e 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -41,8 +41,6 @@ using namespace cvc5::expr;
 
 namespace cvc5 {
 
-thread_local NodeManager* NodeManager::s_current = NULL;
-
 namespace {
 
 /**
@@ -97,6 +95,7 @@ typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAtt
 NodeManager::NodeManager()
     : d_skManager(new SkolemManager),
       d_bvManager(new BoundVarManager),
+      d_initialized(false),
       next_id(0),
       d_attrManager(new expr::attr::AttributeManager()),
       d_nodeUnderDeletion(nullptr),
@@ -104,7 +103,12 @@ NodeManager::NodeManager()
       d_abstractValueCount(0),
       d_skolemCounter(0)
 {
-  init();
+}
+
+NodeManager* NodeManager::currentNM()
+{
+  thread_local static NodeManager nm;
+  return &nm;
 }
 
 bool NodeManager::isNAryKind(Kind k)
@@ -183,10 +187,15 @@ TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs)
 }
 
 void NodeManager::init() {
-  // `mkConst()` indirectly needs the correct NodeManager in scope because we
-  // call `NodeValue::inc()` which uses `NodeManager::curentNM()`
-  NodeManagerScope nms(this);
+  if (d_initialized)
+  {
+    return;
+  }
+  d_initialized = true;
 
+  // Note: This code cannot be part of the constructor because it indirectly
+  // calls `NodeManager::currentNM()`, which is where the `NodeManager` is
+  // being constructed.
   poolInsert( &expr::NodeValue::null() );
 
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
@@ -199,11 +208,6 @@ void NodeManager::init() {
 }
 
 NodeManager::~NodeManager() {
-  // have to ensure "this" is the current NodeManager during
-  // destruction of operators, because they get GCed.
-
-  NodeManagerScope nms(this);
-
   // Destroy skolem and bound var manager before cleaning up attributes and
   // zombies
   d_skManager = nullptr;
@@ -253,7 +257,10 @@ NodeManager::~NodeManager() {
     }
   }
 
-  poolRemove( &expr::NodeValue::null() );
+  if (d_initialized)
+  {
+    poolRemove(&expr::NodeValue::null());
+  }
 
   if(Debug.isOn("gc:leaks")) {
     Debug("gc:leaks") << "still in pool:" << endl;
@@ -434,15 +441,6 @@ std::vector<NodeValue*> NodeManager::TopologicalSort(
 
 TypeNode NodeManager::getType(TNode n, bool check)
 {
-  // Many theories' type checkers call Node::getType() directly.  This
-  // is incorrect, since "this" might not be the caller's current node
-  // manager.  Rather than force the individual typecheckers not to do
-  // this (by policy, which would be imperfect and lead to
-  // hard-to-find bugs, which it has in the past), we just set this
-  // node manager to be current for the duration of this check.
-  //
-  NodeManagerScope nms(this);
-
   TypeNode typeNode;
   bool hasType = getAttribute(n, TypeAttr(), typeNode);
   bool needsCheck = check && !getAttribute(n, TypeCheckedAttr());
@@ -562,7 +560,6 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
     const std::set<TypeNode>& unresolvedTypes,
     uint32_t flags)
 {
-  NodeManagerScope nms(this);
   std::map<std::string, TypeNode> nameResolutions;
   std::vector<TypeNode> dtts;
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index b651c055a..204cdb677 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -90,7 +90,6 @@ class NodeManager
   friend class SkolemManager;
 
   friend class NodeBuilder;
-  friend class NodeManagerScope;
 
  public:
   /**
@@ -101,6 +100,14 @@ class NodeManager
   static bool isNAryKind(Kind k);
 
  private:
+  /**
+   * Instead of creating an instance using the constructor,
+   * `NodeManager::currentNM()` should be used to retrieve an instance of
+   * `NodeManager`.
+   */
+  explicit NodeManager();
+  ~NodeManager();
+
   /** Predicate for use with STL algorithms */
   struct NodeValueReferenceCountNonZero {
     bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
@@ -113,8 +120,6 @@ class NodeManager
                              expr::NodeValueIDHashFunction,
                              expr::NodeValueIDEquality> NodeValueIDSet;
 
-  static thread_local NodeManager* s_current;
-
   /** The skolem manager */
   std::unique_ptr<SkolemManager> d_skManager;
   /** The bound variable manager */
@@ -122,6 +127,8 @@ class NodeManager
 
   NodeValuePool d_nodeValuePool;
 
+  bool d_initialized;
+
   size_t next_id;
 
   expr::attr::AttributeManager* d_attrManager;
@@ -346,8 +353,6 @@ class NodeManager
 
   NodeManager& operator=(const NodeManager&) = delete;
 
-  void init();
-
   /**
    * Create a variable with the given name and type.  NOTE that no
    * lookup is done on the name.  If you mkVar("a", type) and then
@@ -374,11 +379,16 @@ class NodeManager
                 int flags = SKOLEM_DEFAULT);
 
  public:
-  explicit NodeManager();
-  ~NodeManager();
+  /**
+   * Initialize the node manager by adding a null node to the pool and filling
+   * the caches for `operatorOf()`. This method must be called before using the
+   * NodeManager. This method may be called multiple times. Subsequent calls to
+   * this method have no effect.
+   */
+  void init();
 
   /** The node manager in the current public-facing cvc5 library context */
-  static NodeManager* currentNM() { return s_current; }
+  static NodeManager* currentNM();
   /** Get this node manager's skolem manager */
   SkolemManager* getSkolemManager() { return d_skManager.get(); }
   /** Get this node manager's bound variable manager */
@@ -1052,43 +1062,6 @@ class NodeManager
   void debugHook(int debugFlag);
 }; /* class NodeManager */
 
-/**
- * This class changes the "current" thread-global
- * <code>NodeManager</code> when it is created and reinstates the
- * previous thread-global <code>NodeManager</code> when it is
- * destroyed, effectively maintaining a set of nested
- * <code>NodeManager</code> scopes.  This is especially useful on
- * public-interface calls into the cvc5 library, where cvc5's notion
- * of the "current" <code>NodeManager</code> should be set to match
- * the calling context.  See, for example, the implementations of
- * public calls in the <code>SmtEngine</code> class.
- *
- * The client must be careful to create and destroy
- * <code>NodeManagerScope</code> objects in a well-nested manner (such
- * as on the stack). You may create a <code>NodeManagerScope</code>
- * with <code>new</code> and destroy it with <code>delete</code>, or
- * place it as a data member of an object that is, but if the scope of
- * these <code>new</code>/<code>delete</code> pairs isn't properly
- * maintained, the incorrect "current" <code>NodeManager</code>
- * pointer may be restored after a delete.
- */
-class NodeManagerScope {
-  /** The old NodeManager, to be restored on destruction. */
-  NodeManager* d_oldNodeManager;
-public:
- NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current)
- {
-   NodeManager::s_current = nm;
-   Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
-  }
-
-  ~NodeManagerScope() {
-    NodeManager::s_current = d_oldNodeManager;
-    Debug("current") << "node manager scope: "
-                     << "returning to " << NodeManager::s_current << "\n";
-  }
-};/* class NodeManagerScope */
-
 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                                          TypeNode constituentType) {
   CheckArgument(!indexType.isNull(), indexType,
@@ -1310,10 +1283,6 @@ TypeNode NodeManager::mkTypeConst(const T& val) {
 
 template <class NodeClass, class T>
 NodeClass NodeManager::mkConstInternal(const T& val) {
-  // This method indirectly calls `NodeValue::inc()`, which relies on having
-  // the correct `NodeManager` in scope.
-  NodeManagerScope nms(this);
-
   // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
   NVStorage<1> nvStorage;
   expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index a7747c674..6f522bbe8 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -466,10 +466,6 @@ TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){
 }
 
 TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
-
   Assert(!t0.isNull());
   Assert(!t1.isNull());
 
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 2f854f581..89b5b7299 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -852,35 +852,23 @@ inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) {
 template <class AttrKind>
 inline typename AttrKind::value_type TypeNode::
 getAttribute(const AttrKind&) const {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
   return NodeManager::currentNM()->getAttribute(d_nv, AttrKind());
 }
 
 template <class AttrKind>
 inline bool TypeNode::
 hasAttribute(const AttrKind&) const {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
   return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind());
 }
 
 template <class AttrKind>
 inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
   return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret);
 }
 
 template <class AttrKind>
 inline void TypeNode::
 setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
-  Assert(NodeManager::currentNM() != NULL)
-      << "There is no current cvc5::NodeManager associated to this thread.\n"
-         "Perhaps a public-facing function is missing a NodeManagerScope ?";
   NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value);
 }
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 141b0c46c..26997e084 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -74,5 +74,7 @@ int main(int argc, char* argv[])
       main::pExecutor->printStatistics(solver->getDriverOptions().err());
     }
   }
+  // Make sure that the command executor is destroyed before the node manager.
+  main::pExecutor.reset();
   exit(1);
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index aa7534f26..96a1aa8ea 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1256,7 +1256,6 @@ std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void)
         "separation logic theory.";
     throw RecoverableModalException(msg);
   }
-  NodeManagerScope nms(getNodeManager());
   Node heap;
   Node nil;
   TheoryModel* tm = getAvailableModel("get separation logic heap and nil");
@@ -1920,7 +1919,6 @@ void SmtEngine::printStatisticsDiff() const
 
 void SmtEngine::setOption(const std::string& key, const std::string& value)
 {
-  NodeManagerScope nms(getNodeManager());
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
 
   if (Dump.isOn("benchmark"))
@@ -1963,7 +1961,6 @@ bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
 
 std::string SmtEngine::getOption(const std::string& key) const
 {
-  NodeManagerScope nms(getNodeManager());
   NodeManager* nm = d_env->getNodeManager();
 
   Trace("smt") << "SMT getOption(" << key << ")" << endl;
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 98f4c8d70..ebaa73b03 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -41,8 +41,7 @@ ResourceManager* currentResourceManager()
 }
 
 SmtScope::SmtScope(const SmtEngine* smt)
-    : NodeManagerScope(smt->getNodeManager()),
-      d_oldSmtEngine(s_smtEngine_current),
+    : d_oldSmtEngine(s_smtEngine_current),
       d_optionsScope(smt ? &const_cast<SmtEngine*>(smt)->getOptions() : nullptr)
 {
   Assert(smt != NULL);
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index cc231fa3c..f9b024a3b 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -38,7 +38,7 @@ bool smtEngineInScope();
 /** get the current resource manager */
 ResourceManager* currentResourceManager();
 
-class SmtScope : public NodeManagerScope
+class SmtScope
 {
  public:
   SmtScope(const SmtEngine* smt);
diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp
index 6d16e4020..e1b4813ec 100644
--- a/src/theory/arrays/theory_arrays_type_rules.cpp
+++ b/src/theory/arrays/theory_arrays_type_rules.cpp
@@ -92,7 +92,6 @@ TypeNode ArrayStoreTypeRule::computeType(NodeManager* nodeManager,
 bool ArrayStoreTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
 {
   Assert(n.getKind() == kind::STORE);
-  NodeManagerScope nms(nodeManager);
 
   TNode store = n[0];
   TNode index = n[1];
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp
index 6cb1f44e1..503eaf4df 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.cpp
+++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp
@@ -99,7 +99,6 @@ bool DatatypeConstructorTypeRule::computeIsConst(NodeManager* nodeManager,
                                                  TNode n)
 {
   Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
-  NodeManagerScope nms(nodeManager);
   for (TNode::const_iterator i = n.begin(); i != n.end(); ++i)
   {
     if (!(*i).isConst())
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 0001b3723..0e8bb62db 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -69,7 +69,7 @@ class TestNodeBlackNode : public TestNode
     Options opts;
     opts.base.outputLanguage = Language::LANG_AST;
     opts.base.outputLanguageWasSetByUser = true;
-    d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
+    d_smt.reset(new SmtEngine(d_nodeManager, &opts));
   }
 
   std::unique_ptr<SmtEngine> d_smt;
@@ -653,7 +653,7 @@ TEST_F(TestNodeBlackNode, dagifier)
 TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node)
 {
   const std::vector<Node> skolems =
-      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+      makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
   Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
   std::vector<Node> children;
   for (Node child : add)
@@ -667,7 +667,7 @@ TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node)
 TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode)
 {
   const std::vector<Node> skolems =
-      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+      makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
   Node add = d_nodeManager->mkNode(kind::PLUS, skolems);
   std::vector<TNode> children;
   for (TNode child : add)
@@ -681,7 +681,7 @@ TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode)
 TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node)
 {
   const std::vector<Node> skolems =
-      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+      makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
   Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
   TNode add_tnode = add_node;
   std::vector<Node> children;
@@ -696,7 +696,7 @@ TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node)
 TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode)
 {
   const std::vector<Node> skolems =
-      makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
+      makeNSkolemNodes(d_nodeManager, 3, d_nodeManager->integerType());
   Node add_node = d_nodeManager->mkNode(kind::PLUS, skolems);
   TNode add_tnode = add_node;
   std::vector<TNode> children;
@@ -801,8 +801,8 @@ TNode level1(NodeManager* nm) { return level0(nm); }
 TEST_F(TestNodeBlackNode, node_tnode_usage)
 {
   Node n;
-  ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get()));
-  ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0");
+  ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager));
+  ASSERT_DEATH(n = level1(d_nodeManager), "d_nv->d_rc > 0");
 }
 
 }  // namespace test
diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp
index fc8b6fb7b..05ccfc90c 100644
--- a/test/unit/node/node_builder_black.cpp
+++ b/test/unit/node/node_builder_black.cpp
@@ -62,14 +62,14 @@ TEST_F(TestNodeBlackNodeBuilder, ctors)
   ASSERT_EQ(spec.getKind(), d_specKind);
   ASSERT_EQ(spec.getNumChildren(), 0u);
 
-  NodeBuilder from_nm(d_nodeManager.get());
+  NodeBuilder from_nm(d_nodeManager);
   ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND);
 #ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(from_nm.getNumChildren(),
                "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
-  NodeBuilder from_nm_kind(d_nodeManager.get(), d_specKind);
+  NodeBuilder from_nm_kind(d_nodeManager, d_specKind);
   ASSERT_EQ(from_nm_kind.getKind(), d_specKind);
   ASSERT_EQ(from_nm_kind.getNumChildren(), 0u);
 
diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp
index d8db32a4b..d3d05040f 100644
--- a/test/unit/node/type_node_white.cpp
+++ b/test/unit/node/type_node_white.cpp
@@ -36,7 +36,7 @@ class TestNodeWhiteTypeNode : public TestNode
   void SetUp() override
   {
     TestNode::SetUp();
-    d_smt.reset(new SmtEngine(d_nodeManager.get()));
+    d_smt.reset(new SmtEngine(d_nodeManager));
   }
   std::unique_ptr<SmtEngine> d_smt;
 };
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 68758f766..329c565ea 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -2053,16 +2053,16 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_nary_partial)
           bv::utils::mkExtract(
               d_nodeManager->mkNode(kind::BITVECTOR_CONCAT, zero, zz), 7, 0)));
 
-  NodeBuilder nbx(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nbx(d_nodeManager, kind::BITVECTOR_MULT);
   nbx << d_x << d_one << x;
   Node x_mul_one_mul_xx = nbx.constructNode();
-  NodeBuilder nby(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nby(d_nodeManager, kind::BITVECTOR_MULT);
   nby << d_y << y << d_one;
   Node y_mul_yy_mul_one = nby.constructNode();
-  NodeBuilder nbz(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nbz(d_nodeManager, kind::BITVECTOR_MULT);
   nbz << d_three << d_z << z;
   Node three_mul_z_mul_zz = nbz.constructNode();
-  NodeBuilder nbz2(d_nodeManager.get(), kind::BITVECTOR_MULT);
+  NodeBuilder nbz2(d_nodeManager, kind::BITVECTOR_MULT);
   nbz2 << d_z << d_nine << z;
   Node z_mul_nine_mul_zz = nbz2.constructNode();
 
diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp
index bc5bfe8f1..46bea5e19 100644
--- a/test/unit/prop/cnf_stream_white.cpp
+++ b/test/unit/prop/cnf_stream_white.cpp
@@ -150,7 +150,6 @@ class TestPropWhiteCnfStream : public TestSmt
 
 TEST_F(TestPropWhiteCnfStream, and)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
@@ -161,7 +160,6 @@ TEST_F(TestPropWhiteCnfStream, and)
 
 TEST_F(TestPropWhiteCnfStream, complex_expr)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
@@ -184,21 +182,18 @@ TEST_F(TestPropWhiteCnfStream, complex_expr)
 
 TEST_F(TestPropWhiteCnfStream, true)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false);
   ASSERT_TRUE(d_satSolver->addClauseCalled());
 }
 
 TEST_F(TestPropWhiteCnfStream, false)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false);
   ASSERT_TRUE(d_satSolver->addClauseCalled());
 }
 
 TEST_F(TestPropWhiteCnfStream, iff)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
@@ -208,7 +203,6 @@ TEST_F(TestPropWhiteCnfStream, iff)
 
 TEST_F(TestPropWhiteCnfStream, implies)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
@@ -218,7 +212,6 @@ TEST_F(TestPropWhiteCnfStream, implies)
 
 TEST_F(TestPropWhiteCnfStream, not )
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
       d_nodeManager->mkNode(kind::NOT, a), false, false);
@@ -227,7 +220,6 @@ TEST_F(TestPropWhiteCnfStream, not )
 
 TEST_F(TestPropWhiteCnfStream, or)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
@@ -238,7 +230,6 @@ TEST_F(TestPropWhiteCnfStream, or)
 
 TEST_F(TestPropWhiteCnfStream, var)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(a, false, false);
@@ -250,7 +241,6 @@ TEST_F(TestPropWhiteCnfStream, var)
 
 TEST_F(TestPropWhiteCnfStream, xor)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
@@ -260,7 +250,6 @@ TEST_F(TestPropWhiteCnfStream, xor)
 
 TEST_F(TestPropWhiteCnfStream, ensure_literal)
 {
-  NodeManagerScope nms(d_nodeManager.get());
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b);
diff --git a/test/unit/test_env.h b/test/unit/test_env.h
index a0c7c68c3..b3f60a98a 100644
--- a/test/unit/test_env.h
+++ b/test/unit/test_env.h
@@ -33,13 +33,12 @@ class TestEnv : public TestInternal
   void SetUp() override
   {
     d_options.reset(new Options());
-    d_nodeManager.reset(new NodeManager());
-    d_env.reset(new Env(d_nodeManager.get(), d_options.get()));
+    d_nodeManager = NodeManager::currentNM();
+    d_env.reset(new Env(d_nodeManager, d_options.get()));
   }
 
-
   std::unique_ptr<Options> d_options;
-  std::unique_ptr<NodeManager> d_nodeManager;
+  NodeManager* d_nodeManager;
   std::unique_ptr<Env> d_env;
 };
 
diff --git a/test/unit/test_node.h b/test/unit/test_node.h
index 4250bb7da..a6a85b1b1 100644
--- a/test/unit/test_node.h
+++ b/test/unit/test_node.h
@@ -30,17 +30,16 @@ class TestNode : public TestInternal
  protected:
   void SetUp() override
   {
-    d_nodeManager.reset(new NodeManager());
+    d_nodeManager = NodeManager::currentNM();
+    d_nodeManager->init();
     d_skolemManager = d_nodeManager->getSkolemManager();
-    d_scope.reset(new NodeManagerScope(d_nodeManager.get()));
     d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType()));
     d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2)));
     d_intTypeNode.reset(new TypeNode(d_nodeManager->integerType()));
     d_realTypeNode.reset(new TypeNode(d_nodeManager->realType()));
   }
 
-  std::unique_ptr<NodeManagerScope> d_scope;
-  std::unique_ptr<NodeManager> d_nodeManager;
+  NodeManager* d_nodeManager;
   SkolemManager* d_skolemManager;
   std::unique_ptr<TypeNode> d_boolTypeNode;
   std::unique_ptr<TypeNode> d_bvTypeNode;
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index 1cc6b0507..92701d60c 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -44,15 +44,14 @@ class TestSmt : public TestInternal
  protected:
   void SetUp() override
   {
-    d_nodeManager.reset(new NodeManager());
+    d_nodeManager = NodeManager::currentNM();
+    d_nodeManager->init();
     d_skolemManager = d_nodeManager->getSkolemManager();
-    d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
-    d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
+    d_smtEngine.reset(new SmtEngine(d_nodeManager));
     d_smtEngine->finishInit();
   }
 
-  std::unique_ptr<NodeManagerScope> d_nmScope;
-  std::unique_ptr<NodeManager> d_nodeManager;
+  NodeManager* d_nodeManager;
   SkolemManager* d_skolemManager;
   std::unique_ptr<SmtEngine> d_smtEngine;
 };
@@ -62,14 +61,13 @@ class TestSmtNoFinishInit : public TestInternal
  protected:
   void SetUp() override
   {
-    d_nodeManager.reset(new NodeManager());
+    d_nodeManager = NodeManager::currentNM();
+    d_nodeManager->init();
     d_skolemManager = d_nodeManager->getSkolemManager();
-    d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
-    d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
+    d_smtEngine.reset(new SmtEngine(d_nodeManager));
   }
 
-  std::unique_ptr<NodeManagerScope> d_nmScope;
-  std::unique_ptr<NodeManager> d_nodeManager;
+  NodeManager* d_nodeManager;
   SkolemManager* d_skolemManager;
   std::unique_ptr<SmtEngine> d_smtEngine;
 };
diff --git a/test/unit/theory/theory_arith_cad_white.cpp b/test/unit/theory/theory_arith_cad_white.cpp
index 3d5f7a8c5..0a2bcb532 100644
--- a/test/unit/theory/theory_arith_cad_white.cpp
+++ b/test/unit/theory/theory_arith_cad_white.cpp
@@ -51,7 +51,7 @@ class TestTheoryWhiteArithCAD : public TestSmt
     d_realType.reset(new TypeNode(d_nodeManager->realType()));
     d_intType.reset(new TypeNode(d_nodeManager->integerType()));
     Trace.on("cad-check");
-    nodeManager = d_nodeManager.get();
+    nodeManager = d_nodeManager;
   }
 
   Node dummy(int i) const { return d_nodeManager->mkConst(Rational(i)); }
diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp
index eace59c96..682ae5bb2 100644
--- a/test/unit/theory/theory_bags_type_rules_white.cpp
+++ b/test/unit/theory/theory_bags_type_rules_white.cpp
@@ -88,9 +88,9 @@ TEST_F(TestTheoryWhiteBagsTypeRule, mkBag_operator)
                                        d_nodeManager->mkConst(Rational(1)));
 
   // only positive multiplicity are constants
-  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), negative));
-  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), zero));
-  ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager.get(), positive));
+  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, negative));
+  ASSERT_FALSE(MkBagTypeRule::computeIsConst(d_nodeManager, zero));
+  ASSERT_TRUE(MkBagTypeRule::computeIsConst(d_nodeManager, positive));
 }
 
 TEST_F(TestTheoryWhiteBagsTypeRule, from_set_operator)