Add Env class (#6093)

This class contains all globally available utilities for internal code.

9 files changed, 476 insertions, 188 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9124977ef..3fc12c585 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -223,6 +223,8 @@ libcvc4_add_sources(
   smt/dump.h
   smt/dump_manager.cpp
   smt/dump_manager.h
+  smt/env.cpp
+  smt/env.h
   smt/expand_definitions.cpp
   smt/expand_definitions.h
   smt/listeners.cpp
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
new file mode 100644
index 000000000..0b6607c35
--- /dev/null
+++ b/src/smt/env.cpp
@@ -0,0 +1,111 @@
+/*********************                                                        */
+/*! \file env.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Smt Environment, main access to global utilities available to
+ ** internal code.
+ **/
+
+#include "smt/env.h"
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "expr/term_conversion_proof_generator.h"
+#include "options/base_options.h"
+#include "printer/printer.h"
+#include "smt/dump_manager.h"
+#include "smt/smt_engine_stats.h"
+#include "theory/rewriter.h"
+#include "util/resource_manager.h"
+
+using namespace CVC4::smt;
+
+namespace CVC4 {
+
+Env::Env(NodeManager* nm)
+    : d_context(new context::Context()),
+      d_userContext(new context::UserContext()),
+      d_nodeManager(nm),
+      d_proofNodeManager(nullptr),
+      d_rewriter(new theory::Rewriter()),
+      d_dumpManager(new DumpManager(d_userContext.get())),
+      d_logic(),
+      d_statisticsRegistry(nullptr),
+      d_resourceManager(nullptr)
+{
+}
+
+Env::~Env() {}
+
+void Env::setOptions(Options* optr)
+{
+  if (optr != nullptr)
+  {
+    // if we provided a set of options, copy their values to the options
+    // owned by this Env.
+    d_options.copyValues(*optr);
+  }
+}
+
+void Env::setStatisticsRegistry(StatisticsRegistry* statReg)
+{
+  d_statisticsRegistry = statReg;
+  // now initialize resource manager
+  d_resourceManager.reset(new ResourceManager(*statReg, d_options));
+}
+
+void Env::setProofNodeManager(ProofNodeManager* pnm)
+{
+  d_proofNodeManager = pnm;
+  d_rewriter->setProofNodeManager(pnm);
+}
+
+void Env::shutdown()
+{
+  d_rewriter.reset(nullptr);
+  d_dumpManager.reset(nullptr);
+  // d_resourceManager must be destroyed before d_statisticsRegistry
+  d_resourceManager.reset(nullptr);
+}
+
+context::UserContext* Env::getUserContext() { return d_userContext.get(); }
+
+context::Context* Env::getContext() { return d_context.get(); }
+
+NodeManager* Env::getNodeManager() const { return d_nodeManager; }
+
+ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
+
+theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); }
+
+DumpManager* Env::getDumpManager() { return d_dumpManager.get(); }
+
+const LogicInfo& Env::getLogicInfo() const { return d_logic; }
+
+StatisticsRegistry* Env::getStatisticsRegistry()
+{
+  return d_statisticsRegistry;
+}
+
+const Options& Env::getOptions() const { return d_options; }
+
+ResourceManager* Env::getResourceManager() const
+{
+  return d_resourceManager.get();
+}
+
+const Printer& Env::getPrinter()
+{
+  return *Printer::getPrinter(d_options[options::outputLanguage]);
+}
+
+std::ostream& Env::getDumpOut() { return *d_options.getOut(); }
+
+}  // namespace CVC4
diff --git a/src/smt/env.h b/src/smt/env.h
new file mode 100644
index 000000000..e8f73a4f2
--- /dev/null
+++ b/src/smt/env.h
@@ -0,0 +1,187 @@
+/*********************                                                        */
+/*! \file env.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Smt Environment, main access to global utilities available to
+ ** internal code
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__SMT__ENV_H
+#define CVC4__SMT__ENV_H
+
+#include <memory>
+
+#include "options/options.h"
+#include "theory/logic_info.h"
+#include "util/sexpr.h"
+#include "util/statistics.h"
+
+namespace CVC4 {
+
+class NodeManager;
+class StatisticsRegistry;
+class ProofNodeManager;
+class Printer;
+class ResourceManager;
+
+namespace context {
+class Context;
+class UserContext;
+}  // namespace context
+
+namespace smt {
+class DumpManager;
+}
+
+namespace theory {
+class Rewriter;
+}
+
+/**
+ * The environment class.
+ *
+ * This class lives in the SmtEngine and contains all utilities that are
+ * globally available to all internal code.
+ */
+class Env
+{
+  friend class SmtEngine;
+
+ public:
+  /**
+   * Construct an Env with the given node manager.
+   */
+  Env(NodeManager* nm);
+  /** Destruct the env.  */
+  ~Env();
+
+  /* Access to members------------------------------------------------------- */
+  /** Get a pointer to the Context owned by this Env. */
+  context::Context* getContext();
+
+  /** Get a pointer to the UserContext owned by this Env. */
+  context::UserContext* getUserContext();
+
+  /** Get a pointer to the underlying NodeManager. */
+  NodeManager* getNodeManager() const;
+
+  /**
+   * Get the underlying proof node manager. Note since proofs depend on option
+   * initialization, this is only available after the SmtEngine that owns this
+   * environment is initialized, and only non-null if proofs are enabled.
+   */
+  ProofNodeManager* getProofNodeManager();
+
+  /** Get a pointer to the Rewriter owned by this Env. */
+  theory::Rewriter* getRewriter();
+
+  /** Get a pointer to the underlying dump manager. */
+  smt::DumpManager* getDumpManager();
+
+  /** Get the options object (const version only) owned by this Env. */
+  const Options& getOptions() const;
+
+  /** Get the resource manager owned by this Env. */
+  ResourceManager* getResourceManager() const;
+
+  /** Get the logic information currently set. */
+  const LogicInfo& getLogicInfo() const;
+
+  /** Get a pointer to the StatisticsRegistry. */
+  StatisticsRegistry* getStatisticsRegistry();
+
+  /* Option helpers---------------------------------------------------------- */
+
+  /**
+   * Get the current printer based on the current options
+   * @return the current printer
+   */
+  const Printer& getPrinter();
+
+  /**
+   * Get the output stream that --dump=X should print to
+   * @return the output stream
+   */
+  std::ostream& getDumpOut();
+
+ private:
+  /* Private initialization ------------------------------------------------- */
+
+  /** Set options, which makes a deep copy of optr if non-null */
+  void setOptions(Options* optr = nullptr);
+  /** Set the statistics registry */
+  void setStatisticsRegistry(StatisticsRegistry* statReg);
+  /** Set proof node manager if it exists */
+  void setProofNodeManager(ProofNodeManager* pnm);
+
+  /* Private shutdown ------------------------------------------------------- */
+  /**
+   * Shutdown method, which destroys the non-essential members of this class
+   * in preparation for destroying SMT engine.
+   */
+  void shutdown();
+  /* Members ---------------------------------------------------------------- */
+
+  /** The SAT context owned by this Env */
+  std::unique_ptr<context::Context> d_context;
+  /** User level context owned by this Env */
+  std::unique_ptr<context::UserContext> d_userContext;
+  /**
+   * A pointer to the node manager of this environment. A node manager is
+   * not necessarily unique to an SmtEngine instance.
+   */
+  NodeManager* d_nodeManager;
+  /**
+   * A pointer to the proof node manager, which is non-null if proofs are
+   * enabled. This is owned by the proof manager of the SmtEngine that owns
+   * this environment.
+   */
+  ProofNodeManager* d_proofNodeManager;
+  /**
+   * The rewriter owned by this Env. We have a different instance
+   * of the rewriter for each Env instance. This is because rewriters may
+   * hold references to objects that belong to theory solvers, which are
+   * specific to an SmtEngine/TheoryEngine instance.
+   */
+  std::unique_ptr<theory::Rewriter> d_rewriter;
+  /** The dump manager */
+  std::unique_ptr<smt::DumpManager> d_dumpManager;
+  /**
+   * The logic we're in. This logic may be an extension of the logic set by the
+   * user, which may be different from the user-provided logic due to the
+   * options we have set.
+   *
+   * This is the authorative copy of the logic that internal subsolvers should
+   * consider during solving and initialization.
+   */
+  LogicInfo d_logic;
+  /**
+   * The statistics registry, which is owned by the SmtEngine that owns this.
+   */
+  StatisticsRegistry* d_statisticsRegistry;
+  /**
+   * The options object, which contains the modified version of the options
+   * provided as input to the SmtEngine that owns this environment. Note
+   * that d_options may be modified by the options manager, e.g. based
+   * on the input logic.
+   *
+   * This is the authorative copy of the options that internal subsolvers should
+   * consider during solving and initialization.
+   */
+  Options d_options;
+  /** Manager for limiting time and abstract resource usage. */
+  std::unique_ptr<ResourceManager> d_resourceManager;
+}; /* class Env */
+
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__ENV_H */
diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp
index 31b55a4f9..e01d5879e 100644
--- a/src/smt/output_manager.cpp
+++ b/src/smt/output_manager.cpp
@@ -22,10 +22,7 @@ namespace CVC4 {
 
 OutputManager::OutputManager(SmtEngine* smt) : d_smt(smt) {}
 
-const Printer& OutputManager::getPrinter() const
-{
-  return *d_smt->getPrinter();
-}
+const Printer& OutputManager::getPrinter() const { return d_smt->getPrinter(); }
 
 std::ostream& OutputManager::getDumpOut() const
 {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7e8a4fb86..d89b30c87 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -42,6 +42,7 @@
 #include "smt/defined_function.h"
 #include "smt/dump.h"
 #include "smt/dump_manager.h"
+#include "smt/env.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
 #include "smt/logic_exception.h"
@@ -81,32 +82,27 @@ using namespace CVC4::theory;
 namespace CVC4 {
 
 SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
-    : d_state(new SmtEngineState(*this)),
-      d_nodeManager(nm),
-      d_absValues(new AbstractValues(d_nodeManager)),
+    : d_env(new Env(nm)),
+      d_state(new SmtEngineState(getContext(), getUserContext(), *this)),
+      d_absValues(new AbstractValues(getNodeManager())),
       d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
-      d_dumpm(new DumpManager(getUserContext())),
       d_routListener(new ResourceOutListener(*this)),
-      d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)),
+      d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)),
       d_smtSolver(nullptr),
       d_proofManager(nullptr),
       d_model(nullptr),
       d_checkModels(nullptr),
       d_pfManager(nullptr),
       d_ucManager(nullptr),
-      d_rewriter(new theory::Rewriter()),
       d_definedFunctions(nullptr),
       d_sygusSolver(nullptr),
       d_abductSolver(nullptr),
       d_interpolSolver(nullptr),
       d_quantElimSolver(nullptr),
-      d_logic(),
       d_originalOptions(),
       d_isInternalSubsolver(false),
-      d_statisticsRegistry(nullptr),
       d_stats(nullptr),
       d_outMgr(this),
-      d_resourceManager(nullptr),
       d_optm(nullptr),
       d_pp(nullptr),
       d_scope(nullptr)
@@ -124,20 +120,20 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // On the other hand, this hack breaks use cases where multiple SmtEngine
   // objects are created by the user.
   d_scope.reset(new SmtScope(this));
-  if (optr != nullptr)
-  {
-    // if we provided a set of options, copy their values to the options
-    // owned by this SmtEngine.
-    d_options.copyValues(*optr);
-  }
+  // Set options in the environment, which makes a deep copy of optr if
+  // non-null. This may throw an options exception.
+  d_env->setOptions(optr);
+  // now construct the statistics registry
   d_statisticsRegistry.reset(new StatisticsRegistry());
-  d_resourceManager.reset(
-      new ResourceManager(*d_statisticsRegistry.get(), d_options));
-  d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get()));
+  // initialize the environment, which keeps a pointer to statistics registry
+  // and sets up resource manager
+  d_env->setStatisticsRegistry(d_statisticsRegistry.get());
+  // set the options manager
+  d_optm.reset(new smt::OptionsManager(&getOptions(), getResourceManager()));
   // listen to node manager events
-  d_nodeManager->subscribeEvents(d_snmListener.get());
+  getNodeManager()->subscribeEvents(d_snmListener.get());
   // listen to resource out
-  d_resourceManager->registerListener(d_routListener.get());
+  getResourceManager()->registerListener(d_routListener.get());
   // make statistics
   d_stats.reset(new SmtEngineStatistics());
   // reset the preprocessor
@@ -145,7 +141,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
       *this, getUserContext(), *d_absValues.get(), *d_stats));
   // make the SMT solver
   d_smtSolver.reset(
-      new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats));
+      new SmtSolver(*this, *d_state, getResourceManager(), *d_pp, *d_stats));
   // make the SyGuS solver
   d_sygusSolver.reset(
       new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr));
@@ -185,9 +181,9 @@ Result SmtEngine::getStatusOfLastCommand() const
 }
 context::UserContext* SmtEngine::getUserContext()
 {
-  return d_state->getUserContext();
+  return d_env->getUserContext();
 }
-context::Context* SmtEngine::getContext() { return d_state->getContext(); }
+context::Context* SmtEngine::getContext() { return d_env->getContext(); }
 
 TheoryEngine* SmtEngine::getTheoryEngine()
 {
@@ -212,7 +208,8 @@ void SmtEngine::finishInit()
   // of SMT-LIB 2.6 standard.
 
   // set the logic
-  if (!d_logic.isLocked())
+  const LogicInfo& logic = getLogicInfo();
+  if (!logic.isLocked())
   {
     setLogicInternal();
   }
@@ -223,13 +220,13 @@ void SmtEngine::finishInit()
   // Call finish init on the options manager. This inializes the resource
   // manager based on the options, and sets up the best default options
   // based on our heuristics.
-  d_optm->finishInit(d_logic, d_isInternalSubsolver);
+  d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver);
 
   ProofNodeManager* pnm = nullptr;
   if (options::proof())
   {
     // ensure bound variable uses canonical bound variables
-    d_nodeManager->getBoundVarManager()->enableKeepCacheValues();
+    getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
     // make the proof manager
     d_pfManager.reset(new PfManager(getUserContext(), this));
     PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
@@ -237,8 +234,8 @@ void SmtEngine::finishInit()
     d_ucManager.reset(new UnsatCoreManager());
     // use this proof node manager
     pnm = d_pfManager->getProofNodeManager();
-    // enable proof support in the rewriter
-    d_rewriter->setProofNodeManager(pnm);
+    // enable proof support in the environment/rewriter
+    d_env->setProofNodeManager(pnm);
     // enable it in the assertions pipeline
     d_asserts->setProofGenerator(pppg);
     // enable it in the SmtSolver
@@ -248,7 +245,7 @@ void SmtEngine::finishInit()
   }
 
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
-  d_smtSolver->finishInit(const_cast<const LogicInfo&>(d_logic));
+  d_smtSolver->finishInit(logic);
 
   // now can construct the SMT-level model object
   TheoryEngine* te = d_smtSolver->getTheoryEngine();
@@ -274,17 +271,17 @@ void SmtEngine::finishInit()
   {
       LogicInfo everything;
       everything.lock();
-      getOutputManager().getPrinter().toStreamCmdComment(
+      getPrinter().toStreamCmdComment(
           getOutputManager().getDumpOut(),
           "CVC4 always dumps the most general, all-supported logic (below), as "
           "some internals might require the use of a logic more general than "
           "the input.");
-      getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic(
-          getOutputManager().getDumpOut(), everything.getLogicString());
+      getPrinter().toStreamCmdSetBenchmarkLogic(getOutputManager().getDumpOut(),
+                                                everything.getLogicString());
   }
 
   // initialize the dump manager
-  d_dumpm->finishInit();
+  getDumpManager()->finishInit();
 
   // subsolvers
   if (options::produceAbducts())
@@ -302,7 +299,7 @@ void SmtEngine::finishInit()
       << "The PropEngine has pushed but the SmtEngine "
          "hasn't finished initializing!";
 
-  Assert(d_logic.isLocked());
+  Assert(getLogicInfo().isLocked());
 
   // store that we are finished initializing
   d_state->finishInit();
@@ -313,6 +310,8 @@ void SmtEngine::shutdown() {
   d_state->shutdown();
 
   d_smtSolver->shutdown();
+
+  d_env->shutdown();
 }
 
 SmtEngine::~SmtEngine()
@@ -341,13 +340,11 @@ SmtEngine::~SmtEngine()
 #ifdef CVC4_PROOF
     d_proofManager.reset(nullptr);
 #endif
-    d_rewriter.reset(nullptr);
     d_pfManager.reset(nullptr);
     d_ucManager.reset(nullptr);
 
     d_absValues.reset(nullptr);
     d_asserts.reset(nullptr);
-    d_dumpm.reset(nullptr);
     d_model.reset(nullptr);
 
     d_sygusSolver.reset(nullptr);
@@ -355,16 +352,16 @@ SmtEngine::~SmtEngine()
     d_smtSolver.reset(nullptr);
 
     d_stats.reset(nullptr);
-    d_nodeManager->unsubscribeEvents(d_snmListener.get());
+    getNodeManager()->unsubscribeEvents(d_snmListener.get());
     d_snmListener.reset(nullptr);
     d_routListener.reset(nullptr);
     d_optm.reset(nullptr);
     d_pp.reset(nullptr);
-    // d_resourceManager must be destroyed before d_statisticsRegistry
-    d_resourceManager.reset(nullptr);
     d_statisticsRegistry.reset(nullptr);
     // destroy the state
     d_state.reset(nullptr);
+    // destroy the environment
+    d_env.reset(nullptr);
   } catch(Exception& e) {
     Warning() << "CVC4 threw an exception during cleanup." << endl
               << e << endl;
@@ -379,7 +376,7 @@ void SmtEngine::setLogic(const LogicInfo& logic)
     throw ModalException("Cannot set logic in SmtEngine after the engine has "
                          "finished initializing.");
   }
-  d_logic = logic;
+  d_env->d_logic = logic;
   d_userLogic = logic;
   setLogicInternal();
 }
@@ -393,8 +390,8 @@ void SmtEngine::setLogic(const std::string& s)
     // dump out a set-logic command
     if (Dump.isOn("raw-benchmark"))
     {
-      getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic(
-          getOutputManager().getDumpOut(), d_logic.getLogicString());
+      getPrinter().toStreamCmdSetBenchmarkLogic(
+          getOutputManager().getDumpOut(), getLogicInfo().getLogicString());
     }
   }
   catch (IllegalArgumentException& e)
@@ -405,7 +402,10 @@ void SmtEngine::setLogic(const std::string& s)
 
 void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); }
 
-const LogicInfo& SmtEngine::getLogicInfo() const { return d_logic; }
+const LogicInfo& SmtEngine::getLogicInfo() const
+{
+  return d_env->getLogicInfo();
+}
 
 LogicInfo SmtEngine::getUserLogicInfo() const
 {
@@ -422,7 +422,7 @@ void SmtEngine::notifyStartParsing(std::string filename)
   // Copy the original options. This is called prior to beginning parsing.
   // Hence reset should revert to these options, which note is after reading
   // the command line.
-  d_originalOptions.copyValues(d_options);
+  d_originalOptions.copyValues(getOptions());
 }
 
 const std::string& SmtEngine::getFilename() const
@@ -434,7 +434,7 @@ void SmtEngine::setLogicInternal()
   Assert(!d_state->isFullyInited())
       << "setting logic in SmtEngine but the engine has already"
          " finished initializing for this run";
-  d_logic.lock();
+  d_env->d_logic.lock();
   d_userLogic.lock();
 }
 
@@ -452,12 +452,12 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
           (value == "sat")
               ? Result::SAT
               : ((value == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN);
-      getOutputManager().getPrinter().toStreamCmdSetBenchmarkStatus(
+      getPrinter().toStreamCmdSetBenchmarkStatus(
           getOutputManager().getDumpOut(), status);
     }
     else
     {
-      getOutputManager().getPrinter().toStreamCmdSetInfo(
+      getPrinter().toStreamCmdSetInfo(
           getOutputManager().getDumpOut(), key, value);
     }
   }
@@ -513,7 +513,7 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
   if (key == "all-statistics")
   {
     vector<SExpr> stats;
-    StatisticsRegistry* sr = d_nodeManager->getStatisticsRegistry();
+    StatisticsRegistry* sr = getNodeManager()->getStatisticsRegistry();
     for (StatisticsRegistry::const_iterator i = sr->begin(); i != sr->end();
          ++i)
     {
@@ -671,7 +671,7 @@ void SmtEngine::defineFunction(Node func,
   }
 
   DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula);
-  d_dumpm->addToDump(nc, "declarations");
+  getDumpManager()->addToDump(nc, "declarations");
 
   // type check body
   debugCheckFunctionBody(formula, formals, func);
@@ -726,7 +726,7 @@ void SmtEngine::defineFunctionsRec(
 
   if (Dump.isOn("raw-benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdDefineFunctionRec(
+    getPrinter().toStreamCmdDefineFunctionRec(
         getOutputManager().getDumpOut(), funcs, formals, formulas);
   }
 
@@ -891,8 +891,8 @@ Result SmtEngine::checkSat(const Node& assumption, bool inUnsatCore)
 {
   if (Dump.isOn("benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdCheckSat(
-        getOutputManager().getDumpOut(), assumption);
+    getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut(),
+                                     assumption);
   }
   std::vector<Node> assump;
   if (!assumption.isNull())
@@ -909,13 +909,12 @@ Result SmtEngine::checkSat(const std::vector<Node>& assumptions,
   {
     if (assumptions.empty())
     {
-      getOutputManager().getPrinter().toStreamCmdCheckSat(
-          getOutputManager().getDumpOut());
+      getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut());
     }
     else
     {
-      getOutputManager().getPrinter().toStreamCmdCheckSatAssuming(
-          getOutputManager().getDumpOut(), assumptions);
+      getPrinter().toStreamCmdCheckSatAssuming(getOutputManager().getDumpOut(),
+                                               assumptions);
     }
   }
   return checkSatInternal(assumptions, inUnsatCore, false);
@@ -925,8 +924,7 @@ Result SmtEngine::checkEntailed(const Node& node, bool inUnsatCore)
 {
   if (Dump.isOn("benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdQuery(
-        getOutputManager().getDumpOut(), node);
+    getPrinter().toStreamCmdQuery(getOutputManager().getDumpOut(), node);
   }
   return checkSatInternal(
              node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
@@ -992,13 +990,15 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
     }
 
     return r;
-  } catch (UnsafeInterruptException& e) {
-    AlwaysAssert(d_resourceManager->out());
+  }
+  catch (UnsafeInterruptException& e)
+  {
+    AlwaysAssert(getResourceManager()->out());
     // Notice that we do not notify the state of this result. If we wanted to
     // make the solver resume a working state after an interupt, then we would
     // implement a different callback and use it here, e.g.
     // d_state.notifyCheckSatInterupt.
-    Result::UnknownExplanation why = d_resourceManager->outOfResources()
+    Result::UnknownExplanation why = getResourceManager()->outOfResources()
                                          ? Result::RESOURCEOUT
                                          : Result::TIMEOUT;
     return Result(Result::SAT_UNKNOWN, why, d_state->getFilename());
@@ -1024,7 +1024,7 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void)
   finishInit();
   if (Dump.isOn("benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdGetUnsatAssumptions(
+    getPrinter().toStreamCmdGetUnsatAssumptions(
         getOutputManager().getDumpOut());
   }
   UnsatCore core = getUnsatCoreInternal();
@@ -1048,9 +1048,9 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
 
   Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl;
 
-  if (Dump.isOn("raw-benchmark")) {
-    getOutputManager().getPrinter().toStreamCmdAssert(
-        getOutputManager().getDumpOut(), formula);
+  if (Dump.isOn("raw-benchmark"))
+  {
+    getPrinter().toStreamCmdAssert(getOutputManager().getDumpOut(), formula);
   }
 
   // Substitute out any abstract values in ex
@@ -1072,7 +1072,7 @@ void SmtEngine::declareSygusVar(Node var)
   d_sygusSolver->declareSygusVar(var);
   if (Dump.isOn("raw-benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdDeclareVar(
+    getPrinter().toStreamCmdDeclareVar(
         getOutputManager().getDumpOut(), var, var.getType());
   }
   // don't need to set that the conjecture is stale
@@ -1093,7 +1093,7 @@ void SmtEngine::declareSynthFun(Node func,
 
   if (Dump.isOn("raw-benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdSynthFun(
+    getPrinter().toStreamCmdSynthFun(
         getOutputManager().getDumpOut(), func, vars, isInv, sygusType);
   }
 }
@@ -1113,8 +1113,8 @@ void SmtEngine::assertSygusConstraint(Node constraint)
   d_sygusSolver->assertSygusConstraint(constraint);
   if (Dump.isOn("raw-benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdConstraint(
-        getOutputManager().getDumpOut(), constraint);
+    getPrinter().toStreamCmdConstraint(getOutputManager().getDumpOut(),
+                                       constraint);
   }
 }
 
@@ -1128,7 +1128,7 @@ void SmtEngine::assertSygusInvConstraint(Node inv,
   d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
   if (Dump.isOn("raw-benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdInvConstraint(
+    getPrinter().toStreamCmdInvConstraint(
         getOutputManager().getDumpOut(), inv, pre, trans, post);
   }
 }
@@ -1158,7 +1158,8 @@ Node SmtEngine::simplify(const Node& ex)
 
 Node SmtEngine::expandDefinitions(const Node& ex, bool expandOnly)
 {
-  d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep);
+  getResourceManager()->spendResource(
+      ResourceManager::Resource::PreprocessStep);
 
   SmtScope smts(this);
   finishInit();
@@ -1172,8 +1173,9 @@ Node SmtEngine::getValue(const Node& ex) const
   SmtScope smts(this);
 
   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
-  if(Dump.isOn("benchmark")) {
-    d_outMgr.getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex});
+  if (Dump.isOn("benchmark"))
+  {
+    getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex});
   }
   TypeNode expectedType = ex.getType();
 
@@ -1237,9 +1239,9 @@ Model* SmtEngine::getModel() {
 
   finishInit();
 
-  if(Dump.isOn("benchmark")) {
-    getOutputManager().getPrinter().toStreamCmdGetModel(
-        getOutputManager().getDumpOut());
+  if (Dump.isOn("benchmark"))
+  {
+    getPrinter().toStreamCmdGetModel(getOutputManager().getDumpOut());
   }
 
   Model* m = getAvailableModel("get model");
@@ -1275,8 +1277,7 @@ Result SmtEngine::blockModel()
 
   if (Dump.isOn("benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdBlockModel(
-        getOutputManager().getDumpOut());
+    getPrinter().toStreamCmdBlockModel(getOutputManager().getDumpOut());
   }
 
   Model* m = getAvailableModel("block model");
@@ -1304,8 +1305,8 @@ Result SmtEngine::blockModelValues(const std::vector<Node>& exprs)
 
   if (Dump.isOn("benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdBlockModelValues(
-        getOutputManager().getDumpOut(), exprs);
+    getPrinter().toStreamCmdBlockModelValues(getOutputManager().getDumpOut(),
+                                             exprs);
   }
 
   Model* m = getAvailableModel("block model values");
@@ -1323,14 +1324,14 @@ Result SmtEngine::blockModelValues(const std::vector<Node>& exprs)
 
 std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void)
 {
-  if (!d_logic.isTheoryEnabled(THEORY_SEP))
+  if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
   {
     const char* msg =
         "Cannot obtain separation logic expressions if not using the "
         "separation logic theory.";
     throw RecoverableModalException(msg);
   }
-  NodeManagerScope nms(d_nodeManager);
+  NodeManagerScope nms(getNodeManager());
   Node heap;
   Node nil;
   Model* m = getAvailableModel("get separation logic heap and nil");
@@ -1361,7 +1362,7 @@ std::vector<Node> SmtEngine::getExpandedAssertions()
 
 void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
 {
-  if (!d_logic.isTheoryEnabled(THEORY_SEP))
+  if (!getLogicInfo().isTheoryEnabled(THEORY_SEP))
   {
     const char* msg =
         "Cannot declare heap if not using the separation logic theory.";
@@ -1403,6 +1404,11 @@ void SmtEngine::checkProof()
   }
 }
 
+StatisticsRegistry* SmtEngine::getStatisticsRegistry()
+{
+  return d_statisticsRegistry.get();
+}
+
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
 #if IS_PROOFS_BUILD
@@ -1512,8 +1518,7 @@ UnsatCore SmtEngine::getUnsatCore() {
   finishInit();
   if (Dump.isOn("benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdGetUnsatCore(
-        getOutputManager().getDumpOut());
+    getPrinter().toStreamCmdGetUnsatCore(getOutputManager().getDumpOut());
   }
   return getUnsatCoreInternal();
 }
@@ -1525,8 +1530,7 @@ std::string SmtEngine::getProof()
   finishInit();
   if (Dump.isOn("benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdGetProof(
-        getOutputManager().getDumpOut());
+    getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut());
   }
 #if IS_PROOFS_BUILD
   if (!options::proof())
@@ -1660,8 +1664,11 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict)
 {
   SmtScope smts(this);
   finishInit();
-  if(!d_logic.isPure(THEORY_ARITH) && strict){
-    Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
+  const LogicInfo& logic = getLogicInfo();
+  if (!logic.isPure(THEORY_ARITH) && strict)
+  {
+    Warning() << "Unexpected logic for quantifier elimination " << logic
+              << endl;
   }
   return d_quantElimSolver->getQuantifierElimination(
       *d_asserts, q, doFull, d_isInternalSubsolver);
@@ -1727,9 +1734,9 @@ std::vector<Node> SmtEngine::getAssertions()
   SmtScope smts(this);
   finishInit();
   d_state->doPendingPops();
-  if(Dump.isOn("benchmark")) {
-    getOutputManager().getPrinter().toStreamCmdGetAssertions(
-        getOutputManager().getDumpOut());
+  if (Dump.isOn("benchmark"))
+  {
+    getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut());
   }
   Trace("smt") << "SMT getAssertions()" << endl;
   if(!options::produceAssertions()) {
@@ -1756,8 +1763,7 @@ void SmtEngine::push()
   Trace("smt") << "SMT push()" << endl;
   d_smtSolver->processAssertions(*d_asserts);
   if(Dump.isOn("benchmark")) {
-    getOutputManager().getPrinter().toStreamCmdPush(
-        getOutputManager().getDumpOut());
+    getPrinter().toStreamCmdPush(getOutputManager().getDumpOut());
   }
   d_state->userPush();
 }
@@ -1766,9 +1772,9 @@ void SmtEngine::pop() {
   SmtScope smts(this);
   finishInit();
   Trace("smt") << "SMT pop()" << endl;
-  if(Dump.isOn("benchmark")) {
-    getOutputManager().getPrinter().toStreamCmdPop(
-        getOutputManager().getDumpOut());
+  if (Dump.isOn("benchmark"))
+  {
+    getPrinter().toStreamCmdPop(getOutputManager().getDumpOut());
   }
   d_state->userPop();
 
@@ -1785,17 +1791,18 @@ void SmtEngine::pop() {
 
 void SmtEngine::reset()
 {
-  SmtScope smts(this);
+  // save pointer to the current node manager
+  NodeManager* nm = getNodeManager();
   Trace("smt") << "SMT reset()" << endl;
-  if(Dump.isOn("benchmark")) {
-    getOutputManager().getPrinter().toStreamCmdReset(
-        getOutputManager().getDumpOut());
+  if (Dump.isOn("benchmark"))
+  {
+    getPrinter().toStreamCmdReset(getOutputManager().getDumpOut());
   }
   std::string filename = d_state->getFilename();
   Options opts;
   opts.copyValues(d_originalOptions);
   this->~SmtEngine();
-  new (this) SmtEngine(d_nodeManager, &opts);
+  new (this) SmtEngine(nm, &opts);
   // Restore data set after creation
   notifyStartParsing(filename);
 }
@@ -1810,7 +1817,7 @@ void SmtEngine::resetAssertions()
     // (see solver execution modes in the SMT-LIB standard)
     Assert(getContext()->getLevel() == 0);
     Assert(getUserContext()->getLevel() == 0);
-    d_dumpm->resetAssertions();
+    getDumpManager()->resetAssertions();
     return;
   }
 
@@ -1818,13 +1825,12 @@ void SmtEngine::resetAssertions()
   Trace("smt") << "SMT resetAssertions()" << endl;
   if (Dump.isOn("benchmark"))
   {
-    getOutputManager().getPrinter().toStreamCmdResetAssertions(
-        getOutputManager().getDumpOut());
+    getPrinter().toStreamCmdResetAssertions(getOutputManager().getDumpOut());
   }
 
   d_asserts->clearCurrent();
   d_state->notifyResetAssertions();
-  d_dumpm->resetAssertions();
+  getDumpManager()->resetAssertions();
   // push the state to maintain global context around everything
   d_state->setup();
 
@@ -1841,28 +1847,34 @@ void SmtEngine::interrupt()
   d_smtSolver->interrupt();
 }
 
-void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
-  d_resourceManager->setResourceLimit(units, cumulative);
+void SmtEngine::setResourceLimit(unsigned long units, bool cumulative)
+{
+  getResourceManager()->setResourceLimit(units, cumulative);
 }
 void SmtEngine::setTimeLimit(unsigned long milis)
 {
-  d_resourceManager->setTimeLimit(milis);
+  getResourceManager()->setTimeLimit(milis);
 }
 
-unsigned long SmtEngine::getResourceUsage() const {
-  return d_resourceManager->getResourceUsage();
+unsigned long SmtEngine::getResourceUsage() const
+{
+  return getResourceManager()->getResourceUsage();
 }
 
-unsigned long SmtEngine::getTimeUsage() const {
-  return d_resourceManager->getTimeUsage();
+unsigned long SmtEngine::getTimeUsage() const
+{
+  return getResourceManager()->getTimeUsage();
 }
 
 unsigned long SmtEngine::getResourceRemaining() const
 {
-  return d_resourceManager->getResourceRemaining();
+  return getResourceManager()->getResourceRemaining();
 }
 
-NodeManager* SmtEngine::getNodeManager() const { return d_nodeManager; }
+NodeManager* SmtEngine::getNodeManager() const
+{
+  return d_env->getNodeManager();
+}
 
 Statistics SmtEngine::getStatistics() const
 {
@@ -1876,13 +1888,13 @@ SExpr SmtEngine::getStatistic(std::string name) const
 
 void SmtEngine::flushStatistics(std::ostream& out) const
 {
-  d_nodeManager->getStatisticsRegistry()->flushInformation(out);
+  getNodeManager()->getStatisticsRegistry()->flushInformation(out);
   d_statisticsRegistry->flushInformation(out);
 }
 
 void SmtEngine::safeFlushStatistics(int fd) const
 {
-  d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd);
+  getNodeManager()->getStatisticsRegistry()->safeFlushInformation(fd);
   d_statisticsRegistry->safeFlushInformation(fd);
 }
 
@@ -1900,11 +1912,11 @@ void SmtEngine::setUserAttribute(const std::string& attr,
 
 void SmtEngine::setOption(const std::string& key, const std::string& value)
 {
-    NodeManagerScope nms(d_nodeManager);
+  NodeManagerScope nms(getNodeManager());
   Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
 
   if(Dump.isOn("benchmark")) {
-    getOutputManager().getPrinter().toStreamCmdSetOption(
+    getPrinter().toStreamCmdSetOption(
         getOutputManager().getDumpOut(), key, value);
   }
 
@@ -1932,7 +1944,7 @@ void SmtEngine::setOption(const std::string& key, const std::string& value)
   }
 
   std::string optionarg = value;
-  d_options.setOption(key, optionarg);
+  getOptions().setOption(key, optionarg);
 }
 
 void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
@@ -1941,7 +1953,7 @@ bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
 
 CVC4::SExpr SmtEngine::getOption(const std::string& key) const
 {
-  NodeManagerScope nms(d_nodeManager);
+  NodeManagerScope nms(getNodeManager());
 
   Trace("smt") << "SMT getOption(" << key << ")" << endl;
 
@@ -1959,7 +1971,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
   }
 
   if(Dump.isOn("benchmark")) {
-    d_outMgr.getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
+    getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
   }
 
   if(key == "command-verbosity") {
@@ -1991,25 +2003,24 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
     return SExpr(result);
   }
 
-  return SExpr::parseAtom(d_options.getOption(key));
+  return SExpr::parseAtom(getOptions().getOption(key));
 }
 
-Options& SmtEngine::getOptions() { return d_options; }
+Options& SmtEngine::getOptions() { return d_env->d_options; }
 
-const Options& SmtEngine::getOptions() const { return d_options; }
+const Options& SmtEngine::getOptions() const { return d_env->getOptions(); }
 
-ResourceManager* SmtEngine::getResourceManager()
+ResourceManager* SmtEngine::getResourceManager() const
 {
-  return d_resourceManager.get();
+  return d_env->getResourceManager();
 }
 
-DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); }
+DumpManager* SmtEngine::getDumpManager() { return d_env->getDumpManager(); }
 
-const Printer* SmtEngine::getPrinter() const
-{
-  return Printer::getPrinter(d_options[options::outputLanguage]);
-}
+const Printer& SmtEngine::getPrinter() const { return d_env->getPrinter(); }
 
 OutputManager& SmtEngine::getOutputManager() { return d_outMgr; }
 
+theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); }
+
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 4f10b6bc5..94c11be5b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -33,10 +33,6 @@
 #include "util/sexpr.h"
 #include "util/statistics.h"
 
-// In terms of abstraction, this is below (and provides services to)
-// ValidityChecker and above (and requires the services of)
-// PropEngine.
-
 namespace CVC4 {
 
 template <bool ref_count> class NodeTemplate;
@@ -45,6 +41,7 @@ typedef NodeTemplate<false> TNode;
 class TypeNode;
 struct NodeHashFunction;
 
+class Env;
 class NodeManager;
 class TheoryEngine;
 class ProofManager;
@@ -855,19 +852,19 @@ class CVC4_PUBLIC SmtEngine
   ProofManager* getProofManager() { return d_proofManager.get(); };
 
   /** Get the resource manager of this SMT engine */
-  ResourceManager* getResourceManager();
+  ResourceManager* getResourceManager() const;
 
   /** Permit access to the underlying dump manager. */
   smt::DumpManager* getDumpManager();
 
   /** Get the printer used by this SMT engine */
-  const Printer* getPrinter() const;
+  const Printer& getPrinter() const;
 
   /** Get the output manager for this SMT engine */
   OutputManager& getOutputManager();
 
   /** Get a pointer to the Rewriter owned by this SmtEngine. */
-  theory::Rewriter* getRewriter() { return d_rewriter.get(); }
+  theory::Rewriter* getRewriter();
 
   /** The type of our internal map of defined functions */
   using DefinedFunctionMap =
@@ -896,10 +893,7 @@ class CVC4_PUBLIC SmtEngine
   smt::PfManager* getPfManager() { return d_pfManager.get(); };
 
   /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
-  StatisticsRegistry* getStatisticsRegistry()
-  {
-    return d_statisticsRegistry.get();
-  };
+  StatisticsRegistry* getStatisticsRegistry();
 
   /**
    * Internal method to get an unsatisfiable core (only if immediately preceded
@@ -1048,19 +1042,26 @@ class CVC4_PUBLIC SmtEngine
   api::Solver* d_solver = nullptr;
 
   /**
+   * The statistics registry. Notice that this definition must be before the
+   * other members since it must be destroyed last if exceptions occur in the
+   * constructor of SmtEngine.
+   */
+  std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
+  /**
+   * The environment object, which contains all utilities that are globally
+   * available to internal code.
+   */
+  std::unique_ptr<Env> d_env;
+  /**
    * The state of this SmtEngine, which is responsible for maintaining which
    * SMT mode we are in, the contexts, the last result, etc.
    */
   std::unique_ptr<smt::SmtEngineState> d_state;
 
-  /** Our internal node manager */
-  NodeManager* d_nodeManager;
   /** Abstract values */
   std::unique_ptr<smt::AbstractValues> d_absValues;
   /** Assertions manager */
   std::unique_ptr<smt::Assertions> d_asserts;
-  /** The dump manager */
-  std::unique_ptr<smt::DumpManager> d_dumpm;
   /** Resource out listener */
   std::unique_ptr<smt::ResourceOutListener> d_routListener;
   /** Node manager listener */
@@ -1094,14 +1095,6 @@ class CVC4_PUBLIC SmtEngine
    * from refutations. */
   std::unique_ptr<smt::UnsatCoreManager> d_ucManager;
 
-  /**
-   * The rewriter associated with this SmtEngine. We have a different instance
-   * of the rewriter for each SmtEngine instance. This is because rewriters may
-   * hold references to objects that belong to theory solvers, which are
-   * specific to an SmtEngine/TheoryEngine instance.
-   */
-  std::unique_ptr<theory::Rewriter> d_rewriter;
-
   /** An index of our defined functions */
   DefinedFunctionMap* d_definedFunctions;
 
@@ -1114,17 +1107,16 @@ class CVC4_PUBLIC SmtEngine
   std::unique_ptr<smt::InterpolationSolver> d_interpolSolver;
   /** The solver for quantifier elimination queries */
   std::unique_ptr<smt::QuantElimSolver> d_quantElimSolver;
+
   /**
-   * The logic we're in. This logic may be an extension of the logic set by the
-   * user.
+   * The logic set by the user. The actual logic, which may extend the user's
+   * logic, lives in the Env class.
    */
-  LogicInfo d_logic;
-
-  /** The logic set by the user. */
   LogicInfo d_userLogic;
 
   /**
-   * Keep a copy of the original option settings (for reset()).
+   * Keep a copy of the original option settings (for reset()). The current
+   * options live in the Env object.
    */
   Options d_originalOptions;
 
@@ -1136,22 +1128,11 @@ class CVC4_PUBLIC SmtEngine
    */
   std::map<std::string, Integer> d_commandVerbosity;
 
-  /** The statistics registry */
-  std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
-
   /** The statistics class */
   std::unique_ptr<smt::SmtEngineStatistics> d_stats;
 
-  /** The options object */
-  Options d_options;
-
   /** the output manager for commands */
   mutable OutputManager d_outMgr;
-
-  /**
-   * Manager for limiting time and abstract resource usage.
-   */
-  std::unique_ptr<ResourceManager> d_resourceManager;
   /**
    * The options manager, which is responsible for implementing core options
    * such as those related to time outs and printing. It is also responsible
diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 598e78080..cc528f89c 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -51,7 +51,7 @@ ResourceManager* currentResourceManager()
 }
 
 SmtScope::SmtScope(const SmtEngine* smt)
-    : NodeManagerScope(smt->d_nodeManager),
+    : NodeManagerScope(smt->getNodeManager()),
       d_oldSmtEngine(s_smtEngine_current),
       d_optionsScope(smt ? &const_cast<SmtEngine*>(smt)->getOptions() : nullptr)
 {
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index 1da33cde4..504709942 100644
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -20,10 +20,12 @@
 namespace CVC4 {
 namespace smt {
 
-SmtEngineState::SmtEngineState(SmtEngine& smt)
+SmtEngineState::SmtEngineState(context::Context* c,
+                               context::UserContext* u,
+                               SmtEngine& smt)
     : d_smt(smt),
-      d_context(new context::Context()),
-      d_userContext(new context::UserContext()),
+      d_context(c),
+      d_userContext(u),
       d_pendingPops(0),
       d_fullyInited(false),
       d_queryMade(false),
@@ -233,12 +235,9 @@ void SmtEngineState::popto(int toLevel)
   d_userContext->popto(toLevel);
 }
 
-context::UserContext* SmtEngineState::getUserContext()
-{
-  return d_userContext.get();
-}
+context::UserContext* SmtEngineState::getUserContext() { return d_userContext; }
 
-context::Context* SmtEngineState::getContext() { return d_context.get(); }
+context::Context* SmtEngineState::getContext() { return d_context; }
 
 Result SmtEngineState::getStatus() const { return d_status; }
 
diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h
index 032e15c79..3c3075bf5 100644
--- a/src/smt/smt_engine_state.h
+++ b/src/smt/smt_engine_state.h
@@ -47,7 +47,7 @@ namespace smt {
 class SmtEngineState
 {
  public:
-  SmtEngineState(SmtEngine& smt);
+  SmtEngineState(context::Context* c, context::UserContext* u, SmtEngine& smt);
   ~SmtEngineState() {}
   /**
    * Notify that the expected status of the next check-sat is given by the
@@ -203,9 +203,9 @@ class SmtEngineState
   /** Reference to the SmtEngine */
   SmtEngine& d_smt;
   /** Expr manager context */
-  std::unique_ptr<context::Context> d_context;
+  context::Context* d_context;
   /** User level context */
-  std::unique_ptr<context::UserContext> d_userContext;
+  context::UserContext* d_userContext;
   /** The context levels of user pushes */
   std::vector<int> d_userLevels;