Merge branch 'master' into rmMaybermMaybe

70 files changed, 976 insertions, 1163 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 698c38cae..bc7103f0d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -311,8 +311,6 @@ libcvc5_add_sources(
   smt/node_command.h
   smt/optimization_solver.cpp
   smt/optimization_solver.h
-  smt/options_manager.cpp
-  smt/options_manager.h
   smt/output_manager.cpp
   smt/output_manager.h
   smt/quant_elim_solver.cpp
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index c6b004574..a370a0c47 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -195,10 +195,10 @@ std::string Configuration::copyright() {
          << "  See http://www.ginac.de/CLN for copyright information.\n\n";
     }
     if (Configuration::isBuiltWithGlpk()) {
-      ss << "  glpk-cut-log -  a modified version of GPLK, "
+      ss << "  glpk-cut-log - a modified version of GPLK, "
          << "the GNU Linear Programming Kit\n"
          << "  See http://github.com/timothy-king/glpk-cut-log for copyright"
-         << "information\n\n";
+         << " information\n\n";
     }
   }
 
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 58632aafc..ad74e4ab9 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -227,14 +227,6 @@ name   = "Quantifiers"
   help       = "consider ground terms within bodies of quantified formulas for matching"
 
 [[option]]
-  name       = "strictTriggers"
-  category   = "regular"
-  long       = "strict-triggers"
-  type       = "bool"
-  default    = "false"
-  help       = "only instantiate quantifiers with user patterns based on triggers"
-
-[[option]]
   name       = "relevantTriggers"
   category   = "regular"
   long       = "relevant-triggers"
@@ -388,6 +380,9 @@ name   = "Quantifiers"
 [[option.mode.TRUST]]
   name = "trust"
   help = "When provided, use only user-provided patterns for a quantified formula."
+[[option.mode.STRICT]]
+  name = "trust"
+  help = "When provided, use only user-provided patterns for a quantified formula, and do not use any other instantiation techniques."
 [[option.mode.RESORT]]
   name = "resort"
   help = "Use user-provided patterns only after auto-generated patterns saturate."
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index b6cdfb67b..3ec9899ad 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -19,6 +19,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "options/base_options.h"
+#include "options/smt_options.h"
 #include "printer/printer.h"
 #include "proof/conv_proof_generator.h"
 #include "smt/dump_manager.h"
@@ -64,6 +65,8 @@ void Env::setProofNodeManager(ProofNodeManager* pnm)
   d_topLevelSubs->setProofNodeManager(pnm);
 }
 
+void Env::setFilename(const std::string& filename) { d_filename = filename; }
+
 void Env::shutdown()
 {
   d_rewriter.reset(nullptr);
@@ -80,6 +83,16 @@ NodeManager* Env::getNodeManager() const { return d_nodeManager; }
 
 ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
 
+const std::string& Env::getFilename() const { return d_filename; }
+
+bool Env::isTheoryProofProducing() const
+{
+  return d_proofNodeManager != nullptr
+         && (!d_options.smt.unsatCores
+             || d_options.smt.unsatCoresMode
+                    == options::UnsatCoresMode::FULL_PROOF);
+}
+
 theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); }
 
 theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions()
diff --git a/src/smt/env.h b/src/smt/env.h
index 57b5ad9c7..9887aea08 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -82,6 +82,17 @@ class Env
    */
   ProofNodeManager* getProofNodeManager();
 
+  /** Return the input name, or the empty string if not set */
+  const std::string& getFilename() const;
+
+  /**
+   * Check whether theories should produce proofs as well. Other than whether
+   * the proof node manager is set, theory engine proofs are conditioned on the
+   * relationship between proofs and unsat cores: the unsat cores are in
+   * FULL_PROOF mode, no proofs are generated on theory engine.
+   */
+  bool isTheoryProofProducing() const;
+
   /** Get a pointer to the Rewriter owned by this Env. */
   theory::Rewriter* getRewriter();
 
@@ -125,6 +136,11 @@ class Env
 
   /** Set proof node manager if it exists */
   void setProofNodeManager(ProofNodeManager* pnm);
+  /**
+   * Set that the file name of the current instance is the given string. This
+   * is used for various purposes (e.g. get-info, SZS status).
+   */
+  void setFilename(const std::string& filename);
 
   /* Private shutdown ------------------------------------------------------- */
   /**
@@ -191,6 +207,12 @@ class Env
   const Options* d_originalOptions;
   /** Manager for limiting time and abstract resource usage. */
   std::unique_ptr<ResourceManager> d_resourceManager;
+
+  /**
+   * The input file name or the name set through (set-info :filename ...), if
+   * any.
+   */
+  std::string d_filename;
 }; /* class Env */
 
 }  // namespace cvc5
diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
deleted file mode 100644
index a5dee27ae..000000000
--- a/src/smt/options_manager.cpp
+++ /dev/null
@@ -1,48 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Aina Niemetz
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * Module for managing options of an SmtEngine.
- */
-
-#include "smt/options_manager.h"
-
-#include "base/output.h"
-#include "expr/expr_iomanip.h"
-#include "options/base_options.h"
-#include "options/expr_options.h"
-#include "options/smt_options.h"
-#include "smt/command.h"
-#include "smt/dump.h"
-#include "smt/set_defaults.h"
-#include "util/resource_manager.h"
-
-namespace cvc5 {
-namespace smt {
-
-OptionsManager::OptionsManager(Options* opts) : d_options(opts)
-{
-}
-
-OptionsManager::~OptionsManager() {}
-
-void OptionsManager::notifySetOption(const std::string& key)
-{
-}
-
-void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver)
-{
-  // ensure that our heuristics are properly set up
-  setDefaults(logic, isInternalSubsolver);
-}
-
-}  // namespace smt
-}  // namespace cvc5
diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h
deleted file mode 100644
index e7c9d61cb..000000000
--- a/src/smt/options_manager.h
+++ /dev/null
@@ -1,72 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Tim King, Gereon Kremer
- *
- * This file is part of the cvc5 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.
- * ****************************************************************************
- *
- * Module for managing options of an SmtEngine.
- */
-
-#ifndef CVC5__SMT__OPTIONS_MANAGER_H
-#define CVC5__SMT__OPTIONS_MANAGER_H
-
-#include "options/options_listener.h"
-
-namespace cvc5 {
-
-class LogicInfo;
-class Options;
-class ResourceManager;
-class SmtEngine;
-
-namespace smt {
-
-/**
- * This class is intended to be used by SmtEngine, and is responsible for:
- * (1) Implementing core options including timeouts and output preferences,
- * (2) Setting default values for options based on a logic.
- *
- * Notice that the constructor of this class retroactively sets all
- * necessary options that have already been set in the options object it is
- * given. This is to ensure that the command line arguments, which modified
- * on an options object in the driver, immediately take effect upon creation of
- * this class.
- */
-class OptionsManager : public OptionsListener
-{
- public:
-  OptionsManager(Options* opts);
-  ~OptionsManager();
-  /**
-   * Called when a set option call is made on the options object associated
-   * with this class. This handles all options that should be taken into account
-   * immediately instead of e.g. at SmtEngine::finishInit time. This primarily
-   * includes options related to parsing and output.
-   *
-   * This function call is made after the option has been updated. This means
-   * that the value of the option can be queried in the options object that
-   * this class is listening to.
-   */
-  void notifySetOption(const std::string& key) override;
-  /**
-   * Finish init, which is called at the beginning of SmtEngine::finishInit,
-   * just before solving begins. This initializes the options pertaining to
-   * time limits, and sets the default options.
-   */
-  void finishInit(LogicInfo& logic, bool isInternalSubsolver);
-
- private:
-  /** Reference to the options object */
-  Options* d_options;
-};
-
-}  // namespace smt
-}  // namespace cvc5
-
-#endif /* CVC5__SMT__OPTIONS_MANAGER_H */
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index e23323e6d..12433d8ac 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -46,35 +46,39 @@ using namespace cvc5::theory;
 namespace cvc5 {
 namespace smt {
 
-void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
+SetDefaults::SetDefaults(bool isInternalSubsolver)
+    : d_isInternalSubsolver(isInternalSubsolver)
+{
+}
+
+void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
 {
-  Options& opts = Options::current();
   // implied options
-  if (options::debugCheckModels())
+  if (opts.smt.debugCheckModels)
   {
     opts.smt.checkModels = true;
   }
-  if (options::checkModels() || options::dumpModels())
+  if (opts.smt.checkModels || opts.driver.dumpModels)
   {
     opts.smt.produceModels = true;
   }
-  if (options::checkModels())
+  if (opts.smt.checkModels)
   {
     opts.smt.produceAssignments = true;
   }
   // unsat cores and proofs shenanigans
-  if (options::dumpUnsatCoresFull())
+  if (opts.driver.dumpUnsatCoresFull)
   {
     opts.driver.dumpUnsatCores = true;
   }
-  if (options::checkUnsatCores() || options::dumpUnsatCores()
-      || options::unsatAssumptions() || options::minimalUnsatCores()
-      || options::unsatCoresMode() != options::UnsatCoresMode::OFF)
+  if (opts.smt.checkUnsatCores || opts.driver.dumpUnsatCores
+      || opts.smt.unsatAssumptions || opts.smt.minimalUnsatCores
+      || opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF)
   {
     opts.smt.unsatCores = true;
   }
-  if (options::unsatCores()
-      && options::unsatCoresMode() == options::UnsatCoresMode::OFF)
+  if (opts.smt.unsatCores
+      && opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF)
   {
     if (opts.smt.unsatCoresModeWasSetByUser)
     {
@@ -84,13 +88,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS;
   }
 
-  if (options::checkProofs() || options::dumpProofs())
+  if (opts.smt.checkProofs || opts.driver.dumpProofs)
   {
     opts.smt.produceProofs = true;
   }
 
-  if (options::produceProofs()
-      && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
+  if (opts.smt.produceProofs
+      && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF)
   {
     if (opts.smt.unsatCoresModeWasSetByUser)
     {
@@ -103,7 +107,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // set proofs on if not yet set
-  if (options::unsatCores() && !options::produceProofs())
+  if (opts.smt.unsatCores && !opts.smt.produceProofs)
   {
     if (opts.smt.produceProofsWasSetByUser)
     {
@@ -114,8 +118,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // if unsat cores are disabled, then unsat cores mode should be OFF
-  Assert(options::unsatCores()
-         == (options::unsatCoresMode() != options::UnsatCoresMode::OFF));
+  Assert(opts.smt.unsatCores
+         == (opts.smt.unsatCoresMode != options::UnsatCoresMode::OFF));
 
   if (opts.bv.bitvectorAigSimplificationsWasSetByUser)
   {
@@ -128,12 +132,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.bv.bitvectorAlgebraicSolver = true;
   }
 
-  bool isSygus = language::isInputLangSygus(options::inputLanguage());
+  bool isSygus = language::isInputLangSygus(opts.base.inputLanguage);
   bool usesSygus = isSygus;
 
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  if (opts.bv.bitblastMode == options::BitblastMode::EAGER)
   {
-    if (options::produceModels()
+    if (opts.smt.produceModels
         && (logic.isTheoryEnabled(THEORY_ARRAYS)
             || logic.isTheoryEnabled(THEORY_UF)))
     {
@@ -149,12 +153,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                << "generation" << std::endl;
       opts.bv.bitblastMode = options::BitblastMode::LAZY;
     }
-    else if (!options::incrementalSolving())
+    else if (!opts.base.incrementalSolving)
     {
       opts.smt.ackermann = true;
     }
 
-    if (options::incrementalSolving() && !logic.isPure(THEORY_BV))
+    if (opts.base.incrementalSolving && !logic.isPure(THEORY_BV))
     {
       throw OptionException(
           "Incremental eager bit-blasting is currently "
@@ -163,15 +167,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   /* Disable bit-level propagation by default for the BITBLAST solver. */
-  if (options::bvSolver() == options::BVSolver::BITBLAST)
+  if (opts.bv.bvSolver == options::BVSolver::BITBLAST)
   {
     opts.bv.bitvectorPropagate = false;
   }
 
-  if (options::solveIntAsBV() > 0)
+  if (opts.smt.solveIntAsBV > 0)
   {
     // not compatible with incremental
-    if (options::incrementalSolving())
+    if (opts.base.incrementalSolving)
     {
       throw OptionException(
           "solving integers as bitvectors is currently not supported "
@@ -186,14 +190,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     logic.lock();
   }
 
-  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
+  if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
   {
-    if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+    if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
     {
       throw OptionException(
           "solving bitvectors as integers is incompatible with --bool-to-bv.");
     }
-    if (options::BVAndIntegerGranularity() > 8)
+    if (opts.smt.BVAndIntegerGranularity > 8)
     {
       /**
        * The granularity sets the size of the ITE in each element
@@ -214,7 +218,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // set options about ackermannization
-  if (options::ackermann() && options::produceModels()
+  if (opts.smt.ackermann && opts.smt.produceModels
       && (logic.isTheoryEnabled(THEORY_ARRAYS)
           || logic.isTheoryEnabled(THEORY_UF)))
   {
@@ -228,9 +232,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.smt.ackermann = false;
   }
 
-  if (options::ackermann())
+  if (opts.smt.ackermann)
   {
-    if (options::incrementalSolving())
+    if (opts.base.incrementalSolving)
     {
       throw OptionException(
           "Incremental Ackermannization is currently not supported.");
@@ -259,7 +263,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // technique is experimental. This benchmark set also requires removing ITEs
   // during preprocessing, before repeating simplification. Hence, we enable
   // this by default.
-  if (options::doITESimp())
+  if (opts.smt.doITESimp)
   {
     if (!opts.smt.earlyIteRemovalWasSetByUser)
     {
@@ -280,7 +284,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Trace("smt") << "Turning stringExp on since logic does not have everything "
                     "and string theory is enabled\n";
   }
-  if (options::stringExp() || !options::stringLazyPreproc())
+  if (opts.strings.stringExp || !opts.strings.stringLazyPreproc)
   {
     // We require quantifiers since extended functions reduce using them.
     if (!logic.isQuantified())
@@ -299,7 +303,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   // whether we must disable proofs
   bool disableProofs = false;
-  if (options::globalNegate())
+  if (opts.quantifiers.globalNegate)
   {
     // When global negate answers "unsat", it is not due to showing a set of
     // formulas is unsat. Thus, proofs do not apply.
@@ -307,8 +311,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // new unsat core specific restrictions for proofs
-  if (options::unsatCores()
-      && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
+  if (opts.smt.unsatCores
+      && opts.smt.unsatCoresMode != options::UnsatCoresMode::FULL_PROOF)
   {
     // no fine-graininess
     if (!opts.proof.proofGranularityModeWasSetByUser)
@@ -317,7 +321,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
 
-  if (options::arraysExp())
+  if (opts.arrays.arraysExp)
   {
     if (!logic.isQuantified())
     {
@@ -334,17 +338,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // sygus inference may require datatypes
-  if (!isInternalSubsolver)
+  if (!d_isInternalSubsolver)
   {
-    if (options::produceAbducts()
-        || options::produceInterpols() != options::ProduceInterpols::NONE
-        || options::sygusInference() || options::sygusRewSynthInput())
+    if (opts.smt.produceAbducts
+        || opts.smt.produceInterpols != options::ProduceInterpols::NONE
+        || opts.quantifiers.sygusInference
+        || opts.quantifiers.sygusRewSynthInput)
     {
       // since we are trying to recast as sygus, we assume the input is sygus
       isSygus = true;
       usesSygus = true;
     }
-    else if (options::sygusInst())
+    else if (opts.quantifiers.sygusInst)
     {
       // sygus instantiation uses sygus, but it is not a sygus problem
       usesSygus = true;
@@ -367,11 +372,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // if we requiring disabling proofs, disable them now
-  if (disableProofs && options::produceProofs())
+  if (disableProofs && opts.smt.produceProofs)
   {
     opts.smt.unsatCores = false;
     opts.smt.unsatCoresMode = options::UnsatCoresMode::OFF;
-    if (options::produceProofs())
+    if (opts.smt.produceProofs)
     {
       Notice() << "SmtEngine: turning off produce-proofs." << std::endl;
     }
@@ -381,29 +386,28 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // sygus core connective requires unsat cores
-  if (options::sygusCoreConnective())
+  if (opts.quantifiers.sygusCoreConnective)
   {
     opts.smt.unsatCores = true;
-    if (options::unsatCoresMode() == options::UnsatCoresMode::OFF)
+    if (opts.smt.unsatCoresMode == options::UnsatCoresMode::OFF)
     {
       opts.smt.unsatCoresMode = options::UnsatCoresMode::ASSUMPTIONS;
     }
   }
 
-  if ((options::checkModels() || options::checkSynthSol()
-       || options::produceAbducts()
-       || options::produceInterpols() != options::ProduceInterpols::NONE
-       || options::modelCoresMode() != options::ModelCoresMode::NONE
-       || options::blockModelsMode() != options::BlockModelsMode::NONE
-       || options::produceProofs())
-      && !options::produceAssertions())
+  if ((opts.smt.checkModels || opts.smt.checkSynthSol || opts.smt.produceAbducts
+       || opts.smt.produceInterpols != options::ProduceInterpols::NONE
+       || opts.smt.modelCoresMode != options::ModelCoresMode::NONE
+       || opts.smt.blockModelsMode != options::BlockModelsMode::NONE
+       || opts.smt.produceProofs)
+      && !opts.smt.produceAssertions)
   {
     Notice() << "SmtEngine: turning on produce-assertions to support "
              << "option requiring assertions." << std::endl;
     opts.smt.produceAssertions = true;
   }
 
-  if (options::bvAssertInput() && options::produceProofs())
+  if (opts.bv.bvAssertInput && opts.smt.produceProofs)
   {
     Notice() << "Disabling bv-assert-input since it is incompatible with proofs."
              << std::endl;
@@ -412,8 +416,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   // If proofs are required and the user did not specify a specific BV solver,
   // we make sure to use the proof producing BITBLAST_INTERNAL solver.
-  if (options::produceProofs()
-      && options::bvSolver() != options::BVSolver::BITBLAST_INTERNAL
+  if (opts.smt.produceProofs
+      && opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL
       && !opts.bv.bvSolverWasSetByUser
       && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
   {
@@ -425,14 +429,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // whether we want to force safe unsat cores, i.e., if we are in the default
   // ASSUMPTIONS mode, since other ones are experimental
   bool safeUnsatCores =
-      options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS;
+      opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
 
   // Disable options incompatible with incremental solving, unsat cores or
   // output an error if enabled explicitly. It is also currently incompatible
   // with arithmetic, force the option off.
-  if (options::incrementalSolving() || safeUnsatCores)
+  if (opts.base.incrementalSolving || safeUnsatCores)
   {
-    if (options::unconstrainedSimp())
+    if (opts.smt.unconstrainedSimp)
     {
       if (opts.smt.unconstrainedSimpWasSetByUser)
       {
@@ -451,9 +455,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     // Turn on unconstrained simplification for QF_AUFBV
     if (!opts.smt.unconstrainedSimpWasSetByUser)
     {
-      bool uncSimp = !logic.isQuantified() && !options::produceModels()
-                     && !options::produceAssignments()
-                     && !options::checkModels()
+      bool uncSimp = !logic.isQuantified() && !opts.smt.produceModels
+                     && !opts.smt.produceAssignments && !opts.smt.checkModels
                      && logic.isTheoryEnabled(THEORY_ARRAYS)
                      && logic.isTheoryEnabled(THEORY_BV)
                      && !logic.isTheoryEnabled(THEORY_ARITH);
@@ -463,9 +466,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
 
-  if (options::incrementalSolving())
+  if (opts.base.incrementalSolving)
   {
-    if (options::sygusInference())
+    if (opts.quantifiers.sygusInference)
     {
       if (opts.quantifiers.sygusInferenceWasSetByUser)
       {
@@ -479,7 +482,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
 
-  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
+  if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
   {
     /**
      * Operations on 1 bits are better handled as Boolean operations
@@ -494,7 +497,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // explicitly
   if (safeUnsatCores)
   {
-    if (options::simplificationMode() != options::SimplificationMode::NONE)
+    if (opts.smt.simplificationMode != options::SimplificationMode::NONE)
     {
       if (opts.smt.simplificationModeWasSetByUser)
       {
@@ -507,7 +510,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.smt.simplificationMode = options::SimplificationMode::NONE;
     }
 
-    if (options::learnedRewrite())
+    if (opts.smt.learnedRewrite)
     {
       if (opts.smt.learnedRewriteWasSetByUser)
       {
@@ -519,7 +522,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.smt.learnedRewrite = false;
     }
 
-    if (options::pbRewrites())
+    if (opts.arith.pbRewrites)
     {
       if (opts.arith.pbRewritesWasSetByUser)
       {
@@ -531,7 +534,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.arith.pbRewrites = false;
     }
 
-    if (options::sortInference())
+    if (opts.smt.sortInference)
     {
       if (opts.smt.sortInferenceWasSetByUser)
       {
@@ -542,7 +545,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.smt.sortInference = false;
     }
 
-    if (options::preSkolemQuant())
+    if (opts.quantifiers.preSkolemQuant)
     {
       if (opts.quantifiers.preSkolemQuantWasSetByUser)
       {
@@ -554,7 +557,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.quantifiers.preSkolemQuant = false;
     }
 
-    if (options::bitvectorToBool())
+    if (opts.bv.bitvectorToBool)
     {
       if (opts.bv.bitvectorToBoolWasSetByUser)
       {
@@ -565,7 +568,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.bv.bitvectorToBool = false;
     }
 
-    if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+    if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
     {
       if (opts.bv.boolToBitvectorWasSetByUser)
       {
@@ -576,7 +579,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.bv.boolToBitvector = options::BoolToBVMode::OFF;
     }
 
-    if (options::bvIntroducePow2())
+    if (opts.bv.bvIntroducePow2)
     {
       if (opts.bv.bvIntroducePow2WasSetByUser)
       {
@@ -586,7 +589,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.bv.bvIntroducePow2 = false;
     }
 
-    if (options::repeatSimp())
+    if (opts.smt.repeatSimp)
     {
       if (opts.smt.repeatSimpWasSetByUser)
       {
@@ -596,7 +599,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.smt.repeatSimp = false;
     }
 
-    if (options::globalNegate())
+    if (opts.quantifiers.globalNegate)
     {
       if (opts.quantifiers.globalNegateWasSetByUser)
       {
@@ -607,12 +610,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.quantifiers.globalNegate = false;
     }
 
-    if (options::bitvectorAig())
+    if (opts.bv.bitvectorAig)
     {
       throw OptionException("bitblast-aig not supported with unsat cores");
     }
 
-    if (options::doITESimp())
+    if (opts.smt.doITESimp)
     {
       throw OptionException("ITE simp not supported with unsat cores");
     }
@@ -635,9 +638,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
 
-  if (options::cegqiBv() && logic.isQuantified())
+  if (opts.quantifiers.cegqiBv && logic.isQuantified())
   {
-    if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+    if (opts.bv.boolToBitvector != options::BoolToBVMode::OFF)
     {
       if (opts.bv.boolToBitvectorWasSetByUser)
       {
@@ -652,8 +655,8 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // cases where we need produce models
-  if (!options::produceModels()
-      && (options::produceAssignments() || options::sygusRewSynthCheck()
+  if (!opts.smt.produceModels
+      && (opts.smt.produceAssignments || opts.quantifiers.sygusRewSynthCheck
           || usesSygus))
   {
     Notice() << "SmtEngine: turning on produce-models" << std::endl;
@@ -661,95 +664,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   /////////////////////////////////////////////////////////////////////////////
-  // Theory widening
-  //
-  // Some theories imply the use of other theories to handle certain operators,
-  // e.g. UF to handle partial functions.
+  // Widen logic
   /////////////////////////////////////////////////////////////////////////////
-  bool needsUf = false;
-  // strings require LIA, UF; widen the logic
-  if (logic.isTheoryEnabled(THEORY_STRINGS))
-  {
-    LogicInfo log(logic.getUnlockedCopy());
-    // Strings requires arith for length constraints, and also UF
-    needsUf = true;
-    if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic())
-    {
-      Notice()
-          << "Enabling linear integer arithmetic because strings are enabled"
-          << std::endl;
-      log.enableTheory(THEORY_ARITH);
-      log.enableIntegers();
-      log.arithOnlyLinear();
-    }
-    else if (!logic.areIntegersUsed())
-    {
-      Notice() << "Enabling integer arithmetic because strings are enabled"
-               << std::endl;
-      log.enableIntegers();
-    }
-    logic = log;
-    logic.lock();
-  }
-  if (options::bvAbstraction())
-  {
-    // bv abstraction may require UF
-    Notice() << "Enabling UF because bvAbstraction requires it." << std::endl;
-    needsUf = true;
-  }
-  else if (options::preSkolemQuantNested()
-           && opts.quantifiers.preSkolemQuantNestedWasSetByUser)
-  {
-    // if pre-skolem nested is explictly set, then we require UF. If it is
-    // not explicitly set, it is disabled below if UF is not present.
-    Notice() << "Enabling UF because preSkolemQuantNested requires it."
-             << std::endl;
-    needsUf = true;
-  }
-  if (needsUf
-      // Arrays, datatypes and sets permit Boolean terms and thus require UF
-      || logic.isTheoryEnabled(THEORY_ARRAYS)
-      || logic.isTheoryEnabled(THEORY_DATATYPES)
-      || logic.isTheoryEnabled(THEORY_SETS)
-      || logic.isTheoryEnabled(THEORY_BAGS)
-      // Non-linear arithmetic requires UF to deal with division/mod because
-      // their expansion introduces UFs for the division/mod-by-zero case.
-      // If we are eliminating non-linear arithmetic via solve-int-as-bv,
-      // then this is not required, since non-linear arithmetic will be
-      // eliminated altogether (or otherwise fail at preprocessing).
-      || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
-          && options::solveIntAsBV() == 0)
-      // FP requires UF since there are multiple operators that are partially
-      // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more
-      // details).
-      || logic.isTheoryEnabled(THEORY_FP))
-  {
-    if (!logic.isTheoryEnabled(THEORY_UF))
-    {
-      LogicInfo log(logic.getUnlockedCopy());
-      if (!needsUf)
-      {
-        Notice() << "Enabling UF because " << logic << " requires it."
-                 << std::endl;
-      }
-      log.enableTheory(THEORY_UF);
-      logic = log;
-      logic.lock();
-    }
-  }
-  if (options::arithMLTrick())
-  {
-    if (!logic.areIntegersUsed())
-    {
-      // enable integers
-      LogicInfo log(logic.getUnlockedCopy());
-      Notice() << "Enabling integers because arithMLTrick requires it."
-               << std::endl;
-      log.enableIntegers();
-      logic = log;
-      logic.lock();
-    }
-  }
+  widenLogic(logic, opts);
   /////////////////////////////////////////////////////////////////////////////
 
   // Set the options for the theoryOf
@@ -771,7 +688,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (!opts.uf.ufSymmetryBreakerWasSetByUser)
   {
     bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
-                       && !options::incrementalSolving() && !safeUnsatCores;
+                       && !opts.base.incrementalSolving && !safeUnsatCores;
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
                  << std::endl;
     opts.uf.ufSymmetryBreaker = qf_uf_noinc;
@@ -779,7 +696,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   // If in arrays, set the UF handler to arrays
   if (logic.isTheoryEnabled(THEORY_ARRAYS) && !logic.isHigherOrder()
-      && !options::finiteModelFind()
+      && !opts.quantifiers.finiteModelFind
       && (!logic.isQuantified()
           || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF))))
   {
@@ -826,7 +743,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.smt.repeatSimp = repeatSimp;
   }
 
-  if (options::boolToBitvector() == options::BoolToBVMode::ALL
+  if (opts.bv.boolToBitvector == options::BoolToBVMode::ALL
       && !logic.isTheoryEnabled(THEORY_BV))
   {
     if (opts.bv.boolToBitvectorWasSetByUser)
@@ -999,7 +916,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
 
-  if (options::incrementalSolving())
+  if (opts.base.incrementalSolving)
   {
     // disable modes not supported by incremental
     opts.smt.sortInference = false;
@@ -1014,15 +931,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.quantifiers.finiteModelFind = true;
   }
 
-  if (options::instMaxLevel() != -1)
+  if (opts.quantifiers.instMaxLevel != -1)
   {
     Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"
              << std::endl;
     opts.quantifiers.cegqi = false;
   }
 
-  if ((opts.quantifiers.fmfBoundLazyWasSetByUser && options::fmfBoundLazy())
-      || (opts.quantifiers.fmfBoundIntWasSetByUser && options::fmfBoundInt()))
+  if ((opts.quantifiers.fmfBoundLazyWasSetByUser && opts.quantifiers.fmfBoundLazy)
+      || (opts.quantifiers.fmfBoundIntWasSetByUser && opts.quantifiers.fmfBoundInt))
   {
     opts.quantifiers.fmfBound = true;
     Trace("smt")
@@ -1030,11 +947,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   // now have determined whether fmfBound is on/off
   // apply fmfBound options
-  if (options::fmfBound())
+  if (opts.quantifiers.fmfBound)
   {
     if (!opts.quantifiers.mbqiModeWasSetByUser
-        || (options::mbqiMode() != options::MbqiMode::NONE
-            && options::mbqiMode() != options::MbqiMode::FMC))
+        || (opts.quantifiers.mbqiMode != options::MbqiMode::NONE
+            && opts.quantifiers.mbqiMode != options::MbqiMode::FMC))
     {
       // if bounded integers are set, use no MBQI by default
       opts.quantifiers.mbqiMode = options::MbqiMode::NONE;
@@ -1049,28 +966,28 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.uf.ufHo = true;
     // if higher-order, then current variants of model-based instantiation
     // cannot be used
-    if (options::mbqiMode() != options::MbqiMode::NONE)
+    if (opts.quantifiers.mbqiMode != options::MbqiMode::NONE)
     {
       opts.quantifiers.mbqiMode = options::MbqiMode::NONE;
     }
     if (!opts.quantifiers.hoElimStoreAxWasSetByUser)
     {
       // by default, use store axioms only if --ho-elim is set
-      opts.quantifiers.hoElimStoreAx = options::hoElim();
+      opts.quantifiers.hoElimStoreAx = opts.quantifiers.hoElim;
     }
-    if (!options::assignFunctionValues())
+    if (!opts.theory.assignFunctionValues)
     {
       // must assign function values
       opts.theory.assignFunctionValues = true;
     }
     // Cannot use macros, since lambda lifting and macro elimination are inverse
     // operations.
-    if (options::macrosQuant())
+    if (opts.quantifiers.macrosQuant)
     {
       opts.quantifiers.macrosQuant = false;
     }
     // HOL is incompatible with fmfBound
-    if (options::fmfBound())
+    if (opts.quantifiers.fmfBound)
     {
       if (opts.quantifiers.fmfBoundWasSetByUser
           || opts.quantifiers.fmfBoundLazyWasSetByUser
@@ -1084,14 +1001,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       Trace("smt") << "turning off fmf-bound, since HOL\n";
     }
   }
-  if (options::fmfFunWellDefinedRelevant())
+  if (opts.quantifiers.fmfFunWellDefinedRelevant)
   {
     if (!opts.quantifiers.fmfFunWellDefinedWasSetByUser)
     {
       opts.quantifiers.fmfFunWellDefined = true;
     }
   }
-  if (options::fmfFunWellDefined())
+  if (opts.quantifiers.fmfFunWellDefined)
   {
     if (!opts.quantifiers.finiteModelFindWasSetByUser)
     {
@@ -1101,7 +1018,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 
   // now, have determined whether finite model find is on/off
   // apply finite model finding options
-  if (options::finiteModelFind())
+  if (opts.quantifiers.finiteModelFind)
   {
     // apply conservative quantifiers splitting
     if (!opts.quantifiers.quantDynamicSplitWasSetByUser)
@@ -1110,12 +1027,12 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
     if (!opts.quantifiers.eMatchingWasSetByUser)
     {
-      opts.quantifiers.eMatching = options::fmfInstEngine();
+      opts.quantifiers.eMatching = opts.quantifiers.fmfInstEngine;
     }
     if (!opts.quantifiers.instWhenModeWasSetByUser)
     {
       // instantiate only on last call
-      if (options::eMatching())
+      if (opts.quantifiers.eMatching)
       {
         opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL;
       }
@@ -1126,154 +1043,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // if we are attempting to rewrite everything to SyGuS, use sygus()
   if (usesSygus)
   {
-    if (!options::sygus())
-    {
-      Trace("smt") << "turning on sygus" << std::endl;
-    }
-    opts.quantifiers.sygus = true;
-    // must use Ferrante/Rackoff for real arithmetic
-    if (!opts.quantifiers.cegqiMidpointWasSetByUser)
-    {
-      opts.quantifiers.cegqiMidpoint = true;
-    }
-    // must disable cegqi-bv since it may introduce witness terms, which
-    // cannot appear in synthesis solutions
-    if (!opts.quantifiers.cegqiBvWasSetByUser)
-    {
-      opts.quantifiers.cegqiBv = false;
-    }
-    if (options::sygusRepairConst())
-    {
-      if (!opts.quantifiers.cegqiWasSetByUser)
-      {
-        opts.quantifiers.cegqi = true;
-      }
-    }
-    if (options::sygusInference())
-    {
-      // optimization: apply preskolemization, makes it succeed more often
-      if (!opts.quantifiers.preSkolemQuantWasSetByUser)
-      {
-        opts.quantifiers.preSkolemQuant = true;
-      }
-      if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
-      {
-        opts.quantifiers.preSkolemQuantNested = true;
-      }
-    }
-    // counterexample-guided instantiation for sygus
-    if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser)
-    {
-      opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE;
-    }
-    if (!opts.quantifiers.quantConflictFindWasSetByUser)
-    {
-      opts.quantifiers.quantConflictFind = false;
-    }
-    if (!opts.quantifiers.instNoEntailWasSetByUser)
-    {
-      opts.quantifiers.instNoEntail = false;
-    }
-    if (!opts.quantifiers.cegqiFullEffortWasSetByUser)
-    {
-      // should use full effort cbqi for single invocation and repair const
-      opts.quantifiers.cegqiFullEffort = true;
-    }
-    if (options::sygusRew())
-    {
-      opts.quantifiers.sygusRewSynth = true;
-      opts.quantifiers.sygusRewVerify = true;
-    }
-    if (options::sygusRewSynthInput())
-    {
-      // If we are using synthesis rewrite rules from input, we use
-      // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for
-      // details on this technique.
-      opts.quantifiers.sygusRewSynth = true;
-      // we should not use the extended rewriter, since we are interested
-      // in rewrites that are not in the main rewriter
-      if (!opts.quantifiers.sygusExtRewWasSetByUser)
-      {
-        opts.quantifiers.sygusExtRew = false;
-      }
-    }
-    // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
-    // is one that is specialized for returning a single solution. Non-basic
-    // sygus algorithms currently include the PBE solver, UNIF+PI, static
-    // template inference for invariant synthesis, and single invocation
-    // techniques.
-    bool reqBasicSygus = false;
-    if (options::produceAbducts())
-    {
-      // if doing abduction, we should filter strong solutions
-      if (!opts.quantifiers.sygusFilterSolModeWasSetByUser)
-      {
-        opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG;
-      }
-      // we must use basic sygus algorithms, since e.g. we require checking
-      // a sygus side condition for consistency with axioms.
-      reqBasicSygus = true;
-    }
-    if (options::sygusRewSynth() || options::sygusRewVerify()
-        || options::sygusQueryGen())
-    {
-      // rewrite rule synthesis implies that sygus stream must be true
-      opts.quantifiers.sygusStream = true;
-    }
-    if (options::sygusStream() || options::incrementalSolving())
-    {
-      // Streaming and incremental mode are incompatible with techniques that
-      // focus the search towards finding a single solution.
-      reqBasicSygus = true;
-    }
-    // Now, disable options for non-basic sygus algorithms, if necessary.
-    if (reqBasicSygus)
-    {
-      if (!opts.quantifiers.sygusUnifPbeWasSetByUser)
-      {
-        opts.quantifiers.sygusUnifPbe = false;
-      }
-      if (opts.quantifiers.sygusUnifPiWasSetByUser)
-      {
-        opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE;
-      }
-      if (!opts.quantifiers.sygusInvTemplModeWasSetByUser)
-      {
-        opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE;
-      }
-      if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser)
-      {
-        opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE;
-      }
-    }
-    if (!opts.datatypes.dtRewriteErrorSelWasSetByUser)
-    {
-      opts.datatypes.dtRewriteErrorSel = true;
-    }
-    // do not miniscope
-    if (!opts.quantifiers.miniscopeQuantWasSetByUser)
-    {
-      opts.quantifiers.miniscopeQuant = false;
-    }
-    if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser)
-    {
-      opts.quantifiers.miniscopeQuantFreeVar = false;
-    }
-    if (!opts.quantifiers.quantSplitWasSetByUser)
-    {
-      opts.quantifiers.quantSplit = false;
-    }
-    // do not do macros
-    if (!opts.quantifiers.macrosQuantWasSetByUser)
-    {
-      opts.quantifiers.macrosQuant = false;
-    }
-    // use tangent planes by default, since we want to put effort into
-    // the verification step for sygus queries with non-linear arithmetic
-    if (!opts.arith.nlExtTangentPlanesWasSetByUser)
-    {
-      opts.arith.nlExtTangentPlanes = true;
-    }
+    setDefaultsSygus(opts);
   }
   // counterexample-guided instantiation for non-sygus
   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
@@ -1282,7 +1052,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
            || logic.isTheoryEnabled(THEORY_DATATYPES)
            || logic.isTheoryEnabled(THEORY_BV)
            || logic.isTheoryEnabled(THEORY_FP)))
-      || options::cegqiAll())
+      || opts.quantifiers.cegqiAll)
   {
     if (!opts.quantifiers.cegqiWasSetByUser)
     {
@@ -1297,9 +1067,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       }
     }
   }
-  if (options::cegqi())
+  if (opts.quantifiers.cegqi)
   {
-    if (options::incrementalSolving())
+    if (opts.base.incrementalSolving)
     {
       // cannot do nested quantifier elimination in incremental mode
       opts.quantifiers.cegqiNestedQE = false;
@@ -1314,7 +1084,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       {
         opts.quantifiers.instNoEntail = false;
       }
-      if (!opts.quantifiers.instWhenModeWasSetByUser && options::cegqiModel())
+      if (!opts.quantifiers.instWhenModeWasSetByUser && opts.quantifiers.cegqiModel)
       {
         // only instantiation should happen at last call when model is avaiable
         opts.quantifiers.instWhenMode = options::InstWhenMode::LAST_CALL;
@@ -1325,7 +1095,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       // only supported in pure arithmetic or pure BV
       opts.quantifiers.cegqiNestedQE = false;
     }
-    if (options::globalNegate())
+    if (opts.quantifiers.globalNegate)
     {
       if (!opts.quantifiers.prenexQuantWasSetByUser)
       {
@@ -1334,18 +1104,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
   // implied options...
-  if (options::strictTriggers())
-  {
-    if (!opts.quantifiers.userPatternsQuantWasSetByUser)
-    {
-      opts.quantifiers.userPatternsQuant = options::UserPatMode::TRUST;
-    }
-  }
-  if (opts.quantifiers.qcfModeWasSetByUser || options::qcfTConstraint())
+  if (opts.quantifiers.qcfModeWasSetByUser || opts.quantifiers.qcfTConstraint)
   {
     opts.quantifiers.quantConflictFind = true;
   }
-  if (options::cegqiNestedQE())
+  if (opts.quantifiers.cegqiNestedQE)
   {
     opts.quantifiers.prenexQuantUser = true;
     if (!opts.quantifiers.preSkolemQuantWasSetByUser)
@@ -1354,7 +1117,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
   // for induction techniques
-  if (options::quantInduction())
+  if (opts.quantifiers.quantInduction)
   {
     if (!opts.quantifiers.dtStcInductionWasSetByUser)
     {
@@ -1365,7 +1128,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.quantifiers.intWfInduction = true;
     }
   }
-  if (options::dtStcInduction())
+  if (opts.quantifiers.dtStcInduction)
   {
     // try to remove ITEs from quantified formulas
     if (!opts.quantifiers.iteDtTesterSplitQuantWasSetByUser)
@@ -1377,14 +1140,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       opts.quantifiers.iteLiftQuant = options::IteLiftQuantMode::ALL;
     }
   }
-  if (options::intWfInduction())
+  if (opts.quantifiers.intWfInduction)
   {
     if (!opts.quantifiers.purifyTriggersWasSetByUser)
     {
       opts.quantifiers.purifyTriggers = true;
     }
   }
-  if (options::conjectureNoFilter())
+  if (opts.quantifiers.conjectureNoFilter)
   {
     if (!opts.quantifiers.conjectureFilterActiveTermsWasSetByUser)
     {
@@ -1401,7 +1164,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
   if (opts.quantifiers.conjectureGenPerRoundWasSetByUser)
   {
-    if (options::conjectureGenPerRound() > 0)
+    if (opts.quantifiers.conjectureGenPerRound > 0)
     {
       opts.quantifiers.conjectureGen = true;
     }
@@ -1411,7 +1174,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
   // can't pre-skolemize nested quantifiers without UF theory
-  if (!logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant())
+  if (!logic.isTheoryEnabled(THEORY_UF) && opts.quantifiers.preSkolemQuant)
   {
     if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
     {
@@ -1430,11 +1193,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     // introduces new literals into the search. This includes quantifiers
     // (quantifier instantiation), and the lemma schemas used in non-linear
     // and sets. We also can't use it if models are enabled.
-    if (logic.isTheoryEnabled(THEORY_SETS)
-        || logic.isTheoryEnabled(THEORY_BAGS)
-        || logic.isQuantified()
-        || options::produceModels() || options::produceAssignments()
-        || options::checkModels()
+    if (logic.isTheoryEnabled(THEORY_SETS) || logic.isTheoryEnabled(THEORY_BAGS)
+        || logic.isQuantified() || opts.smt.produceModels
+        || opts.smt.produceAssignments || opts.smt.checkModels
         || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
     {
       opts.prop.minisatUseElim = false;
@@ -1442,15 +1203,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
-      && options::nlRlvMode() != options::NlRlvMode::NONE)
+      && opts.arith.nlRlvMode != options::NlRlvMode::NONE)
   {
-    if (!options::relevanceFilter())
+    if (!opts.theory.relevanceFilter)
     {
       if (opts.theory.relevanceFilterWasSetByUser)
       {
         Warning() << "SmtEngine: turning on relevance filtering to support "
                      "--nl-ext-rlv="
-                  << options::nlRlvMode() << std::endl;
+                  << opts.arith.nlRlvMode << std::endl;
       }
       // must use relevance filtering techniques
       opts.theory.relevanceFilter = true;
@@ -1458,13 +1219,13 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   }
 
   // For now, these array theory optimizations do not support model-building
-  if (options::produceModels() || options::produceAssignments()
-      || options::checkModels())
+  if (opts.smt.produceModels || opts.smt.produceAssignments
+      || opts.smt.checkModels)
   {
     opts.arrays.arraysOptimizeLinear = false;
   }
 
-  if (options::stringFMF() && !opts.strings.stringProcessLoopModeWasSetByUser)
+  if (opts.strings.stringFMF && !opts.strings.stringProcessLoopModeWasSetByUser)
   {
     Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
                     "--strings-fmf enabled"
@@ -1475,29 +1236,29 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   // !!! All options that require disabling models go here
   bool disableModels = false;
   std::string sOptNoModel;
-  if (opts.smt.unconstrainedSimpWasSetByUser && options::unconstrainedSimp())
+  if (opts.smt.unconstrainedSimpWasSetByUser && opts.smt.unconstrainedSimp)
   {
     disableModels = true;
     sOptNoModel = "unconstrained-simp";
   }
-  else if (options::sortInference())
+  else if (opts.smt.sortInference)
   {
     disableModels = true;
     sOptNoModel = "sort-inference";
   }
-  else if (options::minisatUseElim())
+  else if (opts.prop.minisatUseElim)
   {
     disableModels = true;
     sOptNoModel = "minisat-elimination";
   }
-  else if (options::globalNegate())
+  else if (opts.quantifiers.globalNegate)
   {
     disableModels = true;
     sOptNoModel = "global-negate";
   }
   if (disableModels)
   {
-    if (options::produceModels())
+    if (opts.smt.produceModels)
     {
       if (opts.smt.produceModelsWasSetByUser)
       {
@@ -1509,7 +1270,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                << sOptNoModel << std::endl;
       opts.smt.produceModels = false;
     }
-    if (options::produceAssignments())
+    if (opts.smt.produceAssignments)
     {
       if (opts.smt.produceAssignmentsWasSetByUser)
       {
@@ -1522,7 +1283,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
                << sOptNoModel << std::endl;
       opts.smt.produceAssignments = false;
     }
-    if (options::checkModels())
+    if (opts.smt.checkModels)
     {
       if (opts.smt.checkModelsWasSetByUser)
       {
@@ -1537,7 +1298,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     }
   }
 
-  if (options::bitblastMode() == options::BitblastMode::EAGER
+  if (opts.bv.bitblastMode == options::BitblastMode::EAGER
       && !logic.isPure(THEORY_BV) && logic.getLogicString() != "QF_UFBV"
       && logic.getLogicString() != "QF_ABV")
   {
@@ -1551,7 +1312,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   if (logic == LogicInfo("QF_UFNRA"))
   {
 #ifdef CVC5_USE_POLY
-    if (!options::nlCad() && !opts.arith.nlCadWasSetByUser)
+    if (!opts.arith.nlCad && !opts.arith.nlCadWasSetByUser)
     {
       opts.arith.nlCad = true;
       if (!opts.arith.nlExtWasSetByUser)
@@ -1566,7 +1327,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 #endif
   }
 #ifndef CVC5_USE_POLY
-  if (options::nlCad())
+  if (opts.arith.nlCad)
   {
     if (opts.arith.nlCadWasSetByUser)
     {
@@ -1585,5 +1346,245 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
 #endif
 }
 
+void SetDefaults::widenLogic(LogicInfo& logic, Options& opts)
+{
+  bool needsUf = false;
+  // strings require LIA, UF; widen the logic
+  if (logic.isTheoryEnabled(THEORY_STRINGS))
+  {
+    LogicInfo log(logic.getUnlockedCopy());
+    // Strings requires arith for length constraints, and also UF
+    needsUf = true;
+    if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic())
+    {
+      Notice()
+          << "Enabling linear integer arithmetic because strings are enabled"
+          << std::endl;
+      log.enableTheory(THEORY_ARITH);
+      log.enableIntegers();
+      log.arithOnlyLinear();
+    }
+    else if (!logic.areIntegersUsed())
+    {
+      Notice() << "Enabling integer arithmetic because strings are enabled"
+               << std::endl;
+      log.enableIntegers();
+    }
+    logic = log;
+    logic.lock();
+  }
+  if (opts.bv.bvAbstraction)
+  {
+    // bv abstraction may require UF
+    Notice() << "Enabling UF because bvAbstraction requires it." << std::endl;
+    needsUf = true;
+  }
+  else if (opts.quantifiers.preSkolemQuantNested
+           && opts.quantifiers.preSkolemQuantNestedWasSetByUser)
+  {
+    // if pre-skolem nested is explictly set, then we require UF. If it is
+    // not explicitly set, it is disabled below if UF is not present.
+    Notice() << "Enabling UF because preSkolemQuantNested requires it."
+             << std::endl;
+    needsUf = true;
+  }
+  if (needsUf
+      // Arrays, datatypes and sets permit Boolean terms and thus require UF
+      || logic.isTheoryEnabled(THEORY_ARRAYS)
+      || logic.isTheoryEnabled(THEORY_DATATYPES)
+      || logic.isTheoryEnabled(THEORY_SETS)
+      || logic.isTheoryEnabled(THEORY_BAGS)
+      // Non-linear arithmetic requires UF to deal with division/mod because
+      // their expansion introduces UFs for the division/mod-by-zero case.
+      // If we are eliminating non-linear arithmetic via solve-int-as-bv,
+      // then this is not required, since non-linear arithmetic will be
+      // eliminated altogether (or otherwise fail at preprocessing).
+      || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
+          && opts.smt.solveIntAsBV == 0)
+      // FP requires UF since there are multiple operators that are partially
+      // defined (see http://smtlib.cs.uiowa.edu/papers/BTRW15.pdf for more
+      // details).
+      || logic.isTheoryEnabled(THEORY_FP))
+  {
+    if (!logic.isTheoryEnabled(THEORY_UF))
+    {
+      LogicInfo log(logic.getUnlockedCopy());
+      if (!needsUf)
+      {
+        Notice() << "Enabling UF because " << logic << " requires it."
+                 << std::endl;
+      }
+      log.enableTheory(THEORY_UF);
+      logic = log;
+      logic.lock();
+    }
+  }
+  if (opts.arith.arithMLTrick)
+  {
+    if (!logic.areIntegersUsed())
+    {
+      // enable integers
+      LogicInfo log(logic.getUnlockedCopy());
+      Notice() << "Enabling integers because arithMLTrick requires it."
+               << std::endl;
+      log.enableIntegers();
+      logic = log;
+      logic.lock();
+    }
+  }
+}
+
+void SetDefaults::setDefaultsSygus(Options& opts)
+{
+  if (!opts.quantifiers.sygus)
+  {
+    Trace("smt") << "turning on sygus" << std::endl;
+  }
+  opts.quantifiers.sygus = true;
+  // must use Ferrante/Rackoff for real arithmetic
+  if (!opts.quantifiers.cegqiMidpointWasSetByUser)
+  {
+    opts.quantifiers.cegqiMidpoint = true;
+  }
+  // must disable cegqi-bv since it may introduce witness terms, which
+  // cannot appear in synthesis solutions
+  if (!opts.quantifiers.cegqiBvWasSetByUser)
+  {
+    opts.quantifiers.cegqiBv = false;
+  }
+  if (opts.quantifiers.sygusRepairConst)
+  {
+    if (!opts.quantifiers.cegqiWasSetByUser)
+    {
+      opts.quantifiers.cegqi = true;
+    }
+  }
+  if (opts.quantifiers.sygusInference)
+  {
+    // optimization: apply preskolemization, makes it succeed more often
+    if (!opts.quantifiers.preSkolemQuantWasSetByUser)
+    {
+      opts.quantifiers.preSkolemQuant = true;
+    }
+    if (!opts.quantifiers.preSkolemQuantNestedWasSetByUser)
+    {
+      opts.quantifiers.preSkolemQuantNested = true;
+    }
+  }
+  // counterexample-guided instantiation for sygus
+  if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser)
+  {
+    opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::USE;
+  }
+  if (!opts.quantifiers.quantConflictFindWasSetByUser)
+  {
+    opts.quantifiers.quantConflictFind = false;
+  }
+  if (!opts.quantifiers.instNoEntailWasSetByUser)
+  {
+    opts.quantifiers.instNoEntail = false;
+  }
+  if (!opts.quantifiers.cegqiFullEffortWasSetByUser)
+  {
+    // should use full effort cbqi for single invocation and repair const
+    opts.quantifiers.cegqiFullEffort = true;
+  }
+  if (opts.quantifiers.sygusRew)
+  {
+    opts.quantifiers.sygusRewSynth = true;
+    opts.quantifiers.sygusRewVerify = true;
+  }
+  if (opts.quantifiers.sygusRewSynthInput)
+  {
+    // If we are using synthesis rewrite rules from input, we use
+    // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for
+    // details on this technique.
+    opts.quantifiers.sygusRewSynth = true;
+    // we should not use the extended rewriter, since we are interested
+    // in rewrites that are not in the main rewriter
+    if (!opts.quantifiers.sygusExtRewWasSetByUser)
+    {
+      opts.quantifiers.sygusExtRew = false;
+    }
+  }
+  // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
+  // is one that is specialized for returning a single solution. Non-basic
+  // sygus algorithms currently include the PBE solver, UNIF+PI, static
+  // template inference for invariant synthesis, and single invocation
+  // techniques.
+  bool reqBasicSygus = false;
+  if (opts.smt.produceAbducts)
+  {
+    // if doing abduction, we should filter strong solutions
+    if (!opts.quantifiers.sygusFilterSolModeWasSetByUser)
+    {
+      opts.quantifiers.sygusFilterSolMode = options::SygusFilterSolMode::STRONG;
+    }
+    // we must use basic sygus algorithms, since e.g. we require checking
+    // a sygus side condition for consistency with axioms.
+    reqBasicSygus = true;
+  }
+  if (opts.quantifiers.sygusRewSynth || opts.quantifiers.sygusRewVerify
+      || opts.quantifiers.sygusQueryGen)
+  {
+    // rewrite rule synthesis implies that sygus stream must be true
+    opts.quantifiers.sygusStream = true;
+  }
+  if (opts.quantifiers.sygusStream || opts.base.incrementalSolving)
+  {
+    // Streaming and incremental mode are incompatible with techniques that
+    // focus the search towards finding a single solution.
+    reqBasicSygus = true;
+  }
+  // Now, disable options for non-basic sygus algorithms, if necessary.
+  if (reqBasicSygus)
+  {
+    if (!opts.quantifiers.sygusUnifPbeWasSetByUser)
+    {
+      opts.quantifiers.sygusUnifPbe = false;
+    }
+    if (opts.quantifiers.sygusUnifPiWasSetByUser)
+    {
+      opts.quantifiers.sygusUnifPi = options::SygusUnifPiMode::NONE;
+    }
+    if (!opts.quantifiers.sygusInvTemplModeWasSetByUser)
+    {
+      opts.quantifiers.sygusInvTemplMode = options::SygusInvTemplMode::NONE;
+    }
+    if (!opts.quantifiers.cegqiSingleInvModeWasSetByUser)
+    {
+      opts.quantifiers.cegqiSingleInvMode = options::CegqiSingleInvMode::NONE;
+    }
+  }
+  if (!opts.datatypes.dtRewriteErrorSelWasSetByUser)
+  {
+    opts.datatypes.dtRewriteErrorSel = true;
+  }
+  // do not miniscope
+  if (!opts.quantifiers.miniscopeQuantWasSetByUser)
+  {
+    opts.quantifiers.miniscopeQuant = false;
+  }
+  if (!opts.quantifiers.miniscopeQuantFreeVarWasSetByUser)
+  {
+    opts.quantifiers.miniscopeQuantFreeVar = false;
+  }
+  if (!opts.quantifiers.quantSplitWasSetByUser)
+  {
+    opts.quantifiers.quantSplit = false;
+  }
+  // do not do macros
+  if (!opts.quantifiers.macrosQuantWasSetByUser)
+  {
+    opts.quantifiers.macrosQuant = false;
+  }
+  // use tangent planes by default, since we want to put effort into
+  // the verification step for sygus queries with non-linear arithmetic
+  if (!opts.arith.nlExtTangentPlanesWasSetByUser)
+  {
+    opts.arith.nlExtTangentPlanes = true;
+  }
+}
+
 }  // namespace smt
 }  // namespace cvc5
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index 6e77b488c..99db64b4a 100644
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -16,25 +16,49 @@
 #ifndef CVC5__SMT__SET_DEFAULTS_H
 #define CVC5__SMT__SET_DEFAULTS_H
 
+#include "options/options.h"
 #include "theory/logic_info.h"
 
 namespace cvc5 {
 namespace smt {
 
 /**
- * The purpose of this method is to set the default options and update the logic
- * info for an SMT engine.
- *
- * @param logic A reference to the logic of SmtEngine, which can be
- * updated by this method based on the current options and the logic itself.
- * @param isInternalSubsolver Whether we are setting the options for an
- * internal subsolver (see SmtEngine::isInternalSubsolver).
- *
- * NOTE: we currently modify the current options in scope. This method
- * can be further refactored to modify an options object provided as an
- * explicit argument.
+ * Class responsible for setting default options, which includes managing
+ * implied options and dependencies between the options and the logic.
  */
-void setDefaults(LogicInfo& logic, bool isInternalSubsolver);
+class SetDefaults
+{
+ public:
+  /**
+   * @param isInternalSubsolver Whether we are setting the options for an
+   * internal subsolver (see SmtEngine::isInternalSubsolver).
+   */
+  SetDefaults(bool isInternalSubsolver);
+  /**
+   * The purpose of this method is to set the default options and update the
+   * logic info for an SMT engine.
+   *
+   * @param logic A reference to the logic of SmtEngine, which can be
+   * updated by this method based on the current options and the logic itself.
+   * @param opts The options to modify, typically the main options of the
+   * SmtEngine in scope.
+   */
+  void setDefaults(LogicInfo& logic, Options& opts);
+
+ private:
+  /**
+   * Widen logic to theories that are required, since some theories imply the
+   * use of other theories to handle certain operators, e.g. UF to handle
+   * partial functions.
+   */
+  void widenLogic(LogicInfo& logic, Options& opts);
+  /**
+   * Set defaults related to SyGuS, called when SyGuS is enabled.
+   */
+  void setDefaultsSygus(Options& opts);
+  /** Are we an internal subsolver? */
+  bool d_isInternalSubsolver;
+};
 
 }  // namespace smt
 }  // namespace cvc5
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5f3920929..43177a73a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -49,10 +49,10 @@
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
 #include "smt/node_command.h"
-#include "smt/options_manager.h"
 #include "smt/preprocessor.h"
 #include "smt/proof_manager.h"
 #include "smt/quant_elim_solver.h"
+#include "smt/set_defaults.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_engine_state.h"
 #include "smt/smt_engine_stats.h"
@@ -86,7 +86,7 @@ namespace cvc5 {
 
 SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
     : d_env(new Env(nm, optr)),
-      d_state(new SmtEngineState(getContext(), getUserContext(), *this)),
+      d_state(new SmtEngineState(*d_env.get(), *this)),
       d_absValues(new AbstractValues(getNodeManager())),
       d_asserts(new Assertions(*d_env.get(), *d_absValues.get())),
       d_routListener(new ResourceOutListener(*this)),
@@ -103,7 +103,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
       d_isInternalSubsolver(false),
       d_stats(nullptr),
       d_outMgr(this),
-      d_optm(nullptr),
       d_pp(nullptr),
       d_scope(nullptr)
 {
@@ -120,8 +119,6 @@ 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));
-  // set the options manager
-  d_optm.reset(new smt::OptionsManager(&getOptions()));
   // listen to node manager events
   getNodeManager()->subscribeEvents(d_snmListener.get());
   // listen to resource out
@@ -195,10 +192,10 @@ void SmtEngine::finishInit()
   // set the random seed
   Random::getRandom().setSeed(d_env->getOptions().driver.seed);
 
-  // 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_env->d_logic, d_isInternalSubsolver);
+  // Call finish init on the set defaults module. This inializes the logic
+  // and the best default options based on our heuristics.
+  SetDefaults sdefaults(d_isInternalSubsolver);
+  sdefaults.setDefaults(d_env->d_logic, getOptions());
 
   ProofNodeManager* pnm = nullptr;
   if (d_env->getOptions().smt.produceProofs)
@@ -324,7 +321,6 @@ SmtEngine::~SmtEngine()
     getNodeManager()->unsubscribeEvents(d_snmListener.get());
     d_snmListener.reset(nullptr);
     d_routListener.reset(nullptr);
-    d_optm.reset(nullptr);
     d_pp.reset(nullptr);
     // destroy the state
     d_state.reset(nullptr);
@@ -385,7 +381,7 @@ LogicInfo SmtEngine::getUserLogicInfo() const
 
 void SmtEngine::notifyStartParsing(const std::string& filename)
 {
-  d_state->setFilename(filename);
+  d_env->setFilename(filename);
   d_env->getStatisticsRegistry().registerValue<std::string>("driver::filename",
                                                             filename);
   // Copy the original options. This is called prior to beginning parsing.
@@ -395,7 +391,7 @@ void SmtEngine::notifyStartParsing(const std::string& filename)
 
 const std::string& SmtEngine::getFilename() const
 {
-  return d_state->getFilename();
+  return d_env->getFilename();
 }
 
 void SmtEngine::setResultStatistic(const std::string& result) {
@@ -440,7 +436,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
 
   if (key == "filename")
   {
-    d_state->setFilename(value);
+    d_env->setFilename(value);
   }
   else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser)
   {
@@ -732,7 +728,7 @@ void SmtEngine::defineFunctionRec(Node func,
 Result SmtEngine::quickCheck() {
   Assert(d_state->isFullyInited());
   Trace("smt") << "SMT quickCheck()" << endl;
-  const std::string& filename = d_state->getFilename();
+  const std::string& filename = d_env->getFilename();
   return Result(
       Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
 }
@@ -948,7 +944,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
     {
       printStatisticsDiff();
     }
-    return Result(Result::SAT_UNKNOWN, why, d_state->getFilename());
+    return Result(Result::SAT_UNKNOWN, why, d_env->getFilename());
   }
 }
 
@@ -1217,7 +1213,7 @@ Model* SmtEngine::getModel() {
   }
   // set the information on the SMT-level model
   Assert(m != nullptr);
-  m->d_inputName = d_state->getFilename();
+  m->d_inputName = d_env->getFilename();
   m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT);
   return m;
 }
@@ -1607,8 +1603,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   finishInit();
   if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
   {
-    out << "% SZS output start Proof for " << d_state->getFilename()
-        << std::endl;
+    out << "% SZS output start Proof for " << d_env->getFilename() << std::endl;
   }
   QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations");
 
@@ -1698,7 +1693,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   }
   if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
   {
-    out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
+    out << "% SZS output end Proof for " << d_env->getFilename() << std::endl;
   }
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index d00fa0c76..f42d791e2 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -1112,12 +1112,6 @@ class CVC5_EXPORT SmtEngine
   /** the output manager for commands */
   mutable OutputManager d_outMgr;
   /**
-   * The options manager, which is responsible for implementing core options
-   * such as those related to time outs and printing. It is also responsible
-   * for set default options based on the logic.
-   */
-  std::unique_ptr<smt::OptionsManager> d_optm;
-  /**
    * The preprocessor.
    */
   std::unique_ptr<smt::Preprocessor> d_pp;
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index cb0a94123..a61c18384 100644
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -19,17 +19,15 @@
 #include "options/base_options.h"
 #include "options/option_exception.h"
 #include "options/smt_options.h"
+#include "smt/env.h"
 #include "smt/smt_engine.h"
 
 namespace cvc5 {
 namespace smt {
 
-SmtEngineState::SmtEngineState(context::Context* c,
-                               context::UserContext* u,
-                               SmtEngine& smt)
+SmtEngineState::SmtEngineState(Env& env, SmtEngine& smt)
     : d_smt(smt),
-      d_context(c),
-      d_userContext(u),
+      d_env(env),
       d_pendingPops(0),
       d_fullyInited(false),
       d_queryMade(false),
@@ -45,7 +43,7 @@ void SmtEngineState::notifyExpectedStatus(const std::string& status)
   Assert(status == "sat" || status == "unsat" || status == "unknown")
       << "SmtEngineState::notifyExpectedStatus: unexpected status string "
       << status;
-  d_expectedStatus = Result(status, d_filename);
+  d_expectedStatus = Result(status, d_env.getFilename());
 }
 
 void SmtEngineState::notifyResetAssertions()
@@ -57,7 +55,7 @@ void SmtEngineState::notifyResetAssertions()
   }
   // Remember the global push/pop around everything when beyond Start mode
   // (see solver execution modes in the SMT-LIB standard)
-  Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
+  Assert(d_userLevels.size() == 0 && getUserContext()->getLevel() == 1);
   popto(0);
 }
 
@@ -158,7 +156,7 @@ void SmtEngineState::shutdown()
 {
   doPendingPops();
 
-  while (options::incrementalSolving() && d_userContext->getLevel() > 1)
+  while (options::incrementalSolving() && getUserContext()->getLevel() > 1)
   {
     internalPop(true);
   }
@@ -170,11 +168,6 @@ void SmtEngineState::cleanup()
   popto(0);
 }
 
-void SmtEngineState::setFilename(const std::string& filename)
-{
-  d_filename = filename;
-}
-
 void SmtEngineState::userPush()
 {
   if (!options::incrementalSolving())
@@ -187,10 +180,10 @@ void SmtEngineState::userPush()
   // staying symmetric with pop.
   d_smtMode = SmtMode::ASSERT;
 
-  d_userLevels.push_back(d_userContext->getLevel());
+  d_userLevels.push_back(getUserContext()->getLevel());
   internalPush();
   Trace("userpushpop") << "SmtEngineState: pushed to level "
-                       << d_userContext->getLevel() << std::endl;
+                       << getUserContext()->getLevel() << std::endl;
 }
 
 void SmtEngineState::userPop()
@@ -212,37 +205,37 @@ void SmtEngineState::userPop()
   // is no longer in scope!).
   d_smtMode = SmtMode::ASSERT;
 
-  AlwaysAssert(d_userContext->getLevel() > 0);
-  AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
-  while (d_userLevels.back() < d_userContext->getLevel())
+  AlwaysAssert(getUserContext()->getLevel() > 0);
+  AlwaysAssert(d_userLevels.back() < getUserContext()->getLevel());
+  while (d_userLevels.back() < getUserContext()->getLevel())
   {
     internalPop(true);
   }
   d_userLevels.pop_back();
 }
-
+context::Context* SmtEngineState::getContext() { return d_env.getContext(); }
+context::UserContext* SmtEngineState::getUserContext()
+{
+  return d_env.getUserContext();
+}
 void SmtEngineState::push()
 {
-  d_userContext->push();
-  d_context->push();
+  getUserContext()->push();
+  getContext()->push();
 }
 
 void SmtEngineState::pop()
 {
-  d_userContext->pop();
-  d_context->pop();
+  getUserContext()->pop();
+  getContext()->pop();
 }
 
 void SmtEngineState::popto(int toLevel)
 {
-  d_context->popto(toLevel);
-  d_userContext->popto(toLevel);
+  getContext()->popto(toLevel);
+  getUserContext()->popto(toLevel);
 }
 
-context::UserContext* SmtEngineState::getUserContext() { return d_userContext; }
-
-context::Context* SmtEngineState::getContext() { return d_context; }
-
 Result SmtEngineState::getStatus() const { return d_status; }
 
 bool SmtEngineState::isFullyInited() const { return d_fullyInited; }
@@ -255,8 +248,6 @@ size_t SmtEngineState::getNumUserLevels() const { return d_userLevels.size(); }
 
 SmtMode SmtEngineState::getMode() const { return d_smtMode; }
 
-const std::string& SmtEngineState::getFilename() const { return d_filename; }
-
 void SmtEngineState::internalPush()
 {
   Assert(d_fullyInited);
@@ -266,7 +257,7 @@ void SmtEngineState::internalPush()
   {
     // notifies the SmtEngine to process the assertions immediately
     d_smt.notifyPushPre();
-    d_userContext->push();
+    getUserContext()->push();
     // the context push is done inside of the SAT solver
     d_smt.notifyPushPost();
   }
@@ -300,7 +291,7 @@ void SmtEngineState::doPendingPops()
     // the context pop is done inside of the SAT solver
     d_smt.notifyPopPre();
     // pop the context
-    d_userContext->pop();
+    getUserContext()->pop();
     --d_pendingPops;
     // no need for pop post (for now)
   }
diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h
index 042efb4de..f20180672 100644
--- a/src/smt/smt_engine_state.h
+++ b/src/smt/smt_engine_state.h
@@ -27,6 +27,7 @@
 namespace cvc5 {
 
 class SmtEngine;
+class Env;
 
 namespace smt {
 
@@ -48,7 +49,7 @@ namespace smt {
 class SmtEngineState
 {
  public:
-  SmtEngineState(context::Context* c, context::UserContext* u, SmtEngine& smt);
+  SmtEngineState(Env& env, SmtEngine& smt);
   ~SmtEngineState() {}
   /**
    * Notify that the expected status of the next check-sat is given by the
@@ -126,11 +127,6 @@ class SmtEngineState
    * Cleanup, which pops all contexts to level zero.
    */
   void cleanup();
-  /**
-   * Set that the file name of the current instance is the given string. This
-   * is used for various purposes (e.g. get-info, SZS status).
-   */
-  void setFilename(const std::string& filename);
 
   //---------------------------- context management
   /**
@@ -149,10 +145,6 @@ class SmtEngineState
    * the SMT-LIB command pop.
    */
   void userPop();
-  /** Get a pointer to the UserContext owned by this SmtEngine. */
-  context::UserContext* getUserContext();
-  /** Get a pointer to the Context owned by this SmtEngine. */
-  context::Context* getContext();
   //---------------------------- end context management
 
   //---------------------------- queries
@@ -179,11 +171,13 @@ class SmtEngineState
   Result getStatus() const;
   /** Get the SMT mode we are in */
   SmtMode getMode() const;
-  /** return the input name (if any) */
-  const std::string& getFilename() const;
   //---------------------------- end queries
 
  private:
+  /** get the sat context we are using */
+  context::Context* getContext();
+  /** get the user context we are using */
+  context::UserContext* getUserContext();
   /** Pushes the user and SAT contexts */
   void push();
   /** Pops the user and SAT contexts */
@@ -203,10 +197,8 @@ class SmtEngineState
   void internalPop(bool immediate = false);
   /** Reference to the SmtEngine */
   SmtEngine& d_smt;
-  /** Expr manager context */
-  context::Context* d_context;
-  /** User level context */
-  context::UserContext* d_userContext;
+  /** Reference to the env of the parent SmtEngine */
+  Env& d_env;
   /** The context levels of user pushes */
   std::vector<int> d_userLevels;
 
@@ -253,12 +245,6 @@ class SmtEngineState
 
   /** The SMT mode, for details see enumeration above. */
   SmtMode d_smtMode;
-
-  /**
-   * The input file name or the name set through (set-info :filename ...), if
-   * any.
-   */
-  std::string d_filename;
 };
 
 }  // namespace smt
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 503d9d1db..1014b218d 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -52,15 +52,7 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
 {
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine.reset(new TheoryEngine(
-      d_env,
-      // Other than whether d_pm is set, theory engine proofs are conditioned on
-      // the relationshup between proofs and unsat cores: the unsat cores are in
-      // FULL_PROOF mode, no proofs are generated on theory engine.
-      (options::unsatCores()
-       && options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF)
-          ? nullptr
-          : d_pnm));
+  d_theoryEngine.reset(new TheoryEngine(d_env));
 
   // Add the theories
   for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
@@ -141,7 +133,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
 
   Trace("smt") << "SmtSolver::check()" << endl;
 
-  const std::string& filename = d_state.getFilename();
+  const std::string& filename = d_env.getFilename();
   ResourceManager* rm = d_env.getResourceManager();
   if (rm->out())
   {
diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp
index 93d410bf8..3d43077e5 100644
--- a/src/theory/arith/arith_state.cpp
+++ b/src/theory/arith/arith_state.cpp
@@ -21,10 +21,8 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-ArithState::ArithState(context::Context* c,
-                       context::UserContext* u,
-                       Valuation val)
-    : TheoryState(c, u, val), d_parent(nullptr)
+ArithState::ArithState(Env& env, Valuation val)
+    : TheoryState(env, val), d_parent(nullptr)
 {
 }
 
diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h
index a54ae6bf0..0f0f02f02 100644
--- a/src/theory/arith/arith_state.h
+++ b/src/theory/arith/arith_state.h
@@ -38,7 +38,8 @@ class TheoryArithPrivate;
 class ArithState : public TheoryState
 {
  public:
-  ArithState(context::Context* c, context::UserContext* u, Valuation val);
+  ArithState(Env& env,
+             Valuation val);
   ~ArithState() {}
   /** Are we currently in conflict? */
   bool isInConflict() const override;
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index a8b056d45..785127db5 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -48,7 +48,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_extTheory(d_extTheoryCb,
                   containing.getSatContext(),
                   containing.getUserContext(),
-                  containing.getOutputChannel()),
+                  d_im),
       d_model(containing.getSatContext()),
       d_trSlv(d_im, d_model, pnm, containing.getUserContext()),
       d_extState(d_im, d_model, pnm, containing.getUserContext()),
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 2c7187089..37069d8b8 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -35,24 +35,20 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-TheoryArith::TheoryArith(context::Context* c,
-                         context::UserContext* u,
-                         OutputChannel& out,
-                         Valuation valuation,
-                         const LogicInfo& logicInfo,
-                         ProofNodeManager* pnm)
-    : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm),
+TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
+    : Theory(THEORY_ARITH, env, out, valuation),
       d_ppRewriteTimer(smtStatisticsRegistry().registerTimer(
           "theory::arith::ppRewriteTimer")),
-      d_astate(c, u, valuation),
-      d_im(*this, d_astate, pnm),
-      d_ppre(c, pnm),
-      d_bab(d_astate, d_im, d_ppre, pnm),
+      d_astate(env, valuation),
+      d_im(*this, d_astate, d_pnm),
+      d_ppre(getSatContext(), d_pnm),
+      d_bab(d_astate, d_im, d_ppre, d_pnm),
       d_eqSolver(nullptr),
-      d_internal(new TheoryArithPrivate(*this, c, u, d_bab, pnm)),
+      d_internal(new TheoryArithPrivate(
+          *this, getSatContext(), getUserContext(), d_bab, d_pnm)),
       d_nonlinearExtension(nullptr),
-      d_opElim(pnm, logicInfo),
-      d_arithPreproc(d_astate, d_im, pnm, d_opElim),
+      d_opElim(d_pnm, getLogicInfo()),
+      d_arithPreproc(d_astate, d_im, d_pnm, d_opElim),
       d_rewriter(d_opElim)
 {
   // currently a cyclic dependency to TheoryArithPrivate
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index ee99f44e8..4b0c88fd2 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -44,12 +44,7 @@ class TheoryArithPrivate;
 class TheoryArith : public Theory {
   friend class TheoryArithPrivate;
  public:
-  TheoryArith(context::Context* c,
-              context::UserContext* u,
-              OutputChannel& out,
-              Valuation valuation,
-              const LogicInfo& logicInfo,
-              ProofNodeManager* pnm = nullptr);
+  TheoryArith(Env& env, OutputChannel& out, Valuation valuation);
   virtual ~TheoryArith();
 
   //--------------------------------- initialization
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 6c9c162ab..1a6dfedbb 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -55,14 +55,11 @@ const bool d_solveWrite2 = false;
   //bool d_useNonLinearOpt = true;
   //bool d_eagerIndexSplitting = false;
 
-TheoryArrays::TheoryArrays(context::Context* c,
-                           context::UserContext* u,
+TheoryArrays::TheoryArrays(Env& env,
                            OutputChannel& out,
                            Valuation valuation,
-                           const LogicInfo& logicInfo,
-                           ProofNodeManager* pnm,
                            std::string name)
-    : Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name),
+    : Theory(THEORY_ARRAYS, env, out, valuation, name),
       d_numRow(
           smtStatisticsRegistry().registerInt(name + "number of Row lemmas")),
       d_numExt(
@@ -83,37 +80,37 @@ TheoryArrays::TheoryArrays(context::Context* c,
           name + "number of setModelVal splits")),
       d_numSetModelValConflicts(smtStatisticsRegistry().registerInt(
           name + "number of setModelVal conflicts")),
-      d_ppEqualityEngine(u, name + "pp", true),
-      d_ppFacts(u),
-      d_rewriter(pnm),
-      d_state(c, u, valuation),
-      d_im(*this, d_state, pnm),
-      d_literalsToPropagate(c),
-      d_literalsToPropagateIndex(c, 0),
-      d_isPreRegistered(c),
-      d_mayEqualEqualityEngine(c, name + "mayEqual", true),
+      d_ppEqualityEngine(getUserContext(), name + "pp", true),
+      d_ppFacts(getUserContext()),
+      d_rewriter(d_pnm),
+      d_state(env, valuation),
+      d_im(*this, d_state, d_pnm),
+      d_literalsToPropagate(getSatContext()),
+      d_literalsToPropagateIndex(getSatContext(), 0),
+      d_isPreRegistered(getSatContext()),
+      d_mayEqualEqualityEngine(getSatContext(), name + "mayEqual", true),
       d_notify(*this),
-      d_backtracker(c),
-      d_infoMap(c, &d_backtracker, name),
-      d_mergeQueue(c),
+      d_backtracker(getSatContext()),
+      d_infoMap(getSatContext(), &d_backtracker, name),
+      d_mergeQueue(getSatContext()),
       d_mergeInProgress(false),
-      d_RowQueue(c),
-      d_RowAlreadyAdded(u),
-      d_sharedArrays(c),
-      d_sharedOther(c),
-      d_sharedTerms(c, false),
-      d_reads(c),
-      d_constReadsList(c),
+      d_RowQueue(getSatContext()),
+      d_RowAlreadyAdded(getUserContext()),
+      d_sharedArrays(getSatContext()),
+      d_sharedOther(getSatContext()),
+      d_sharedTerms(getSatContext(), false),
+      d_reads(getSatContext()),
+      d_constReadsList(getSatContext()),
       d_constReadsContext(new context::Context()),
-      d_contextPopper(c, d_constReadsContext),
-      d_skolemIndex(c, 0),
-      d_decisionRequests(c),
-      d_permRef(c),
-      d_modelConstraints(c),
-      d_lemmasSaved(c),
-      d_defValues(c),
+      d_contextPopper(getSatContext(), d_constReadsContext),
+      d_skolemIndex(getSatContext(), 0),
+      d_decisionRequests(getSatContext()),
+      d_permRef(getSatContext()),
+      d_modelConstraints(getSatContext()),
+      d_lemmasSaved(getSatContext()),
+      d_defValues(getSatContext()),
       d_readTableContext(new context::Context()),
-      d_arrayMerges(c),
+      d_arrayMerges(getSatContext()),
       d_inCheckModel(false),
       d_dstrat(new TheoryArraysDecisionStrategy(this)),
       d_dstratInit(false)
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 772fc1b79..d255e44f1 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -132,12 +132,9 @@ class TheoryArrays : public Theory {
   IntStat d_numSetModelValConflicts;
 
  public:
-  TheoryArrays(context::Context* c,
-               context::UserContext* u,
+  TheoryArrays(Env& env,
                OutputChannel& out,
                Valuation valuation,
-               const LogicInfo& logicInfo,
-               ProofNodeManager* pnm = nullptr,
                std::string name = "theory::arrays::");
   ~TheoryArrays();
 
diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp
index 6c80e00bd..50c6919fa 100644
--- a/src/theory/bags/solver_state.cpp
+++ b/src/theory/bags/solver_state.cpp
@@ -27,10 +27,7 @@ namespace cvc5 {
 namespace theory {
 namespace bags {
 
-SolverState::SolverState(context::Context* c,
-                         context::UserContext* u,
-                         Valuation val)
-    : TheoryState(c, u, val)
+SolverState::SolverState(Env& env, Valuation val) : TheoryState(env, val)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
index 9c2222e95..68fffacbd 100644
--- a/src/theory/bags/solver_state.h
+++ b/src/theory/bags/solver_state.h
@@ -29,7 +29,8 @@ namespace bags {
 class SolverState : public TheoryState
 {
  public:
-  SolverState(context::Context* c, context::UserContext* u, Valuation val);
+  SolverState(Env& env,
+              Valuation val);
 
   /**
    * This function adds the bag representative n to the set d_bags if it is not
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 580d26c08..f8483064d 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -27,15 +27,10 @@ namespace cvc5 {
 namespace theory {
 namespace bags {
 
-TheoryBags::TheoryBags(context::Context* c,
-                       context::UserContext* u,
-                       OutputChannel& out,
-                       Valuation valuation,
-                       const LogicInfo& logicInfo,
-                       ProofNodeManager* pnm)
-    : Theory(THEORY_BAGS, c, u, out, valuation, logicInfo, pnm),
-      d_state(c, u, valuation),
-      d_im(*this, d_state, pnm),
+TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
+    : Theory(THEORY_BAGS, env, out, valuation),
+      d_state(env, valuation),
+      d_im(*this, d_state, d_pnm),
       d_ig(&d_state, &d_im),
       d_notify(*this, d_im),
       d_statistics(),
diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
index 4ed131e64..671623d05 100644
--- a/src/theory/bags/theory_bags.h
+++ b/src/theory/bags/theory_bags.h
@@ -36,12 +36,7 @@ class TheoryBags : public Theory
 {
  public:
   /** Constructs a new instance of TheoryBags w.r.t. the provided contexts. */
-  TheoryBags(context::Context* c,
-             context::UserContext* u,
-             OutputChannel& out,
-             Valuation valuation,
-             const LogicInfo& logicInfo,
-             ProofNodeManager* pnm);
+  TheoryBags(Env& env, OutputChannel& out, Valuation valuation);
   ~TheoryBags() override;
 
   //--------------------------------- initialization
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 3aac5ecfb..33bb820b4 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -32,13 +32,8 @@ namespace cvc5 {
 namespace theory {
 namespace booleans {
 
-TheoryBool::TheoryBool(context::Context* c,
-                       context::UserContext* u,
-                       OutputChannel& out,
-                       Valuation valuation,
-                       const LogicInfo& logicInfo,
-                       ProofNodeManager* pnm)
-    : Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, pnm)
+TheoryBool::TheoryBool(Env& env, OutputChannel& out, Valuation valuation)
+    : Theory(THEORY_BOOL, env, out, valuation)
 {
 }
 
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index dd574a455..e0b7e6511 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -29,12 +29,7 @@ namespace booleans {
 
 class TheoryBool : public Theory {
  public:
-  TheoryBool(context::Context* c,
-             context::UserContext* u,
-             OutputChannel& out,
-             Valuation valuation,
-             const LogicInfo& logicInfo,
-             ProofNodeManager* pnm = nullptr);
+  TheoryBool(Env& env, OutputChannel& out, Valuation valuation);
 
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 1db03d22b..092bcc9ab 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -25,15 +25,10 @@ namespace cvc5 {
 namespace theory {
 namespace builtin {
 
-TheoryBuiltin::TheoryBuiltin(context::Context* c,
-                             context::UserContext* u,
-                             OutputChannel& out,
-                             Valuation valuation,
-                             const LogicInfo& logicInfo,
-                             ProofNodeManager* pnm)
-    : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, pnm),
-      d_state(c, u, valuation),
-      d_im(*this, d_state, pnm, "theory::builtin::")
+TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation)
+    : Theory(THEORY_BUILTIN, env, out, valuation),
+      d_state(env, valuation),
+      d_im(*this, d_state, d_pnm, "theory::builtin::")
 {
   // indicate we are using the default theory state and inference managers
   d_theoryState = &d_state;
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 72485f0ea..29a3cfb36 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -31,12 +31,7 @@ namespace builtin {
 class TheoryBuiltin : public Theory
 {
  public:
-  TheoryBuiltin(context::Context* c,
-                context::UserContext* u,
-                OutputChannel& out,
-                Valuation valuation,
-                const LogicInfo& logicInfo,
-                ProofNodeManager* pnm = nullptr);
+  TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation);
 
   /** get the official theory rewriter of this theory */
   TheoryRewriter* getTheoryRewriter() override;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 547d24b23..d4926a785 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -30,35 +30,33 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-TheoryBV::TheoryBV(context::Context* c,
-                   context::UserContext* u,
+TheoryBV::TheoryBV(Env& env,
                    OutputChannel& out,
                    Valuation valuation,
-                   const LogicInfo& logicInfo,
-                   ProofNodeManager* pnm,
                    std::string name)
-    : Theory(THEORY_BV, c, u, out, valuation, logicInfo, pnm, name),
+    : Theory(THEORY_BV, env, out, valuation, name),
       d_internal(nullptr),
       d_rewriter(),
-      d_state(c, u, valuation),
+      d_state(env, valuation),
       d_im(*this, d_state, nullptr, "theory::bv::"),
       d_notify(d_im),
-      d_invalidateModelCache(c, true),
+      d_invalidateModelCache(getSatContext(), true),
       d_stats("theory::bv::")
 {
   switch (options::bvSolver())
   {
     case options::BVSolver::BITBLAST:
-      d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm));
+      d_internal.reset(new BVSolverBitblast(&d_state, d_im, d_pnm));
       break;
 
     case options::BVSolver::LAYERED:
-      d_internal.reset(new BVSolverLayered(*this, c, u, pnm, name));
+      d_internal.reset(new BVSolverLayered(
+          *this, getSatContext(), getUserContext(), d_pnm, name));
       break;
 
     default:
       AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL);
-      d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, pnm));
+      d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, d_pnm));
   }
   d_theoryState = &d_state;
   d_inferManager = &d_im;
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index da44d7022..b4afb5f5d 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -39,12 +39,9 @@ class TheoryBV : public Theory
   friend class BVSolverLayered;
 
  public:
-  TheoryBV(context::Context* c,
-           context::UserContext* u,
+  TheoryBV(Env& env,
            OutputChannel& out,
            Valuation valuation,
-           const LogicInfo& logicInfo,
-           ProofNodeManager* pnm = nullptr,
            std::string name = "");
 
   ~TheoryBV();
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 50c955d48..2162c4d14 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -47,24 +47,20 @@ namespace cvc5 {
 namespace theory {
 namespace datatypes {
 
-TheoryDatatypes::TheoryDatatypes(Context* c,
-                                 UserContext* u,
+TheoryDatatypes::TheoryDatatypes(Env& env,
                                  OutputChannel& out,
-                                 Valuation valuation,
-                                 const LogicInfo& logicInfo,
-                                 ProofNodeManager* pnm)
-    : Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, pnm),
-      d_term_sk(u),
-      d_labels(c),
-      d_selector_apps(c),
-      d_collectTermsCache(c),
-      d_collectTermsCacheU(u),
-      d_functionTerms(c),
-      d_singleton_eq(u),
-      d_lemmas_produced_c(u),
+                                 Valuation valuation)
+    : Theory(THEORY_DATATYPES, env, out, valuation),
+      d_term_sk(getUserContext()),
+      d_labels(getSatContext()),
+      d_selector_apps(getSatContext()),
+      d_collectTermsCache(getSatContext()),
+      d_collectTermsCacheU(getUserContext()),
+      d_functionTerms(getSatContext()),
+      d_singleton_eq(getUserContext()),
       d_sygusExtension(nullptr),
-      d_state(c, u, valuation),
-      d_im(*this, d_state, pnm),
+      d_state(env, valuation),
+      d_im(*this, d_state, d_pnm),
       d_notify(d_im, *this)
 {
 
@@ -542,129 +538,151 @@ void TheoryDatatypes::eqNotifyMerge(TNode t1, TNode t2)
 }
 
 void TheoryDatatypes::merge( Node t1, Node t2 ){
-  if (!d_state.isInConflict())
+  if (d_state.isInConflict())
   {
-    Trace("datatypes-merge") << "Merge " << t1 << " " << t2 << std::endl;
-    Assert(areEqual(t1, t2));
-    TNode trep1 = t1;
-    TNode trep2 = t2;
-    EqcInfo* eqc2 = getOrMakeEqcInfo( t2 );
-    if( eqc2 ){
-      bool checkInst = false;
-      if( !eqc2->d_constructor.get().isNull() ){
-        trep2 = eqc2->d_constructor.get();
-      }
-      EqcInfo* eqc1 = getOrMakeEqcInfo( t1 );
-      if( eqc1 ){
-        Trace("datatypes-debug") << "  merge eqc info " << eqc2 << " into " << eqc1 << std::endl;
-        if( !eqc1->d_constructor.get().isNull() ){
-          trep1 = eqc1->d_constructor.get();
-        }
-        //check for clash
-        TNode cons1 = eqc1->d_constructor.get();
-        TNode cons2 = eqc2->d_constructor.get();
-        //if both have constructor, then either clash or unification
-        if( !cons1.isNull() && !cons2.isNull() ){
-          Trace("datatypes-debug") << "  constructors : " << cons1 << " " << cons2 << std::endl;
-          Node unifEq = cons1.eqNode( cons2 );
-          std::vector< Node > rew;
-          if (utils::checkClash(cons1, cons2, rew))
-          {
-            std::vector<Node> conf;
-            conf.push_back(unifEq);
-            Trace("dt-conflict")
-                << "CONFLICT: Clash conflict : " << conf << std::endl;
-            d_im.sendDtConflict(conf, InferenceId::DATATYPES_CLASH_CONFLICT);
-            return;
-          }
-          else
-          {
-            Assert(areEqual(cons1, cons2));
-            //do unification
-            for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
-              if( !areEqual( cons1[i], cons2[i] ) ){
-                Node eq = cons1[i].eqNode( cons2[i] );
-                d_im.addPendingInference(
-                    eq, InferenceId::DATATYPES_UNIF, unifEq);
-                Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl;
-              }
-            }
-          }
-        }
-        Trace("datatypes-debug") << "  instantiated : " << eqc1->d_inst << " " << eqc2->d_inst << std::endl;
-        eqc1->d_inst = eqc1->d_inst || eqc2->d_inst;
-        if( !cons2.isNull() ){
-          if( cons1.isNull() ){
-            Trace("datatypes-debug") << "  must check if it is okay to set the constructor." << std::endl;
-            checkInst = true;
-            addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
-            if (d_state.isInConflict())
-            {
-              return;
-            }
-          }
-        }
-      }else{
-        Trace("datatypes-debug") << "  no eqc info for " << t1 << ", must create" << std::endl;
-        //just copy the equivalence class information
-        eqc1 = getOrMakeEqcInfo( t1, true );
-        eqc1->d_inst.set( eqc2->d_inst );
-        eqc1->d_constructor.set( eqc2->d_constructor );
-        eqc1->d_selectors.set( eqc2->d_selectors );
+    return;
+  }
+  Trace("datatypes-merge") << "Merge " << t1 << " " << t2 << std::endl;
+  Assert(areEqual(t1, t2));
+  TNode trep1 = t1;
+  TNode trep2 = t2;
+  EqcInfo* eqc2 = getOrMakeEqcInfo(t2);
+  if (eqc2 == nullptr)
+  {
+    return;
+  }
+  bool checkInst = false;
+  if (!eqc2->d_constructor.get().isNull())
+  {
+    trep2 = eqc2->d_constructor.get();
+  }
+  EqcInfo* eqc1 = getOrMakeEqcInfo(t1);
+  if (eqc1)
+  {
+    Trace("datatypes-debug")
+        << "  merge eqc info " << eqc2 << " into " << eqc1 << std::endl;
+    if (!eqc1->d_constructor.get().isNull())
+    {
+      trep1 = eqc1->d_constructor.get();
+    }
+    // check for clash
+    TNode cons1 = eqc1->d_constructor.get();
+    TNode cons2 = eqc2->d_constructor.get();
+    // if both have constructor, then either clash or unification
+    if (!cons1.isNull() && !cons2.isNull())
+    {
+      Trace("datatypes-debug")
+          << "  constructors : " << cons1 << " " << cons2 << std::endl;
+      Node unifEq = cons1.eqNode(cons2);
+      std::vector<Node> rew;
+      if (utils::checkClash(cons1, cons2, rew))
+      {
+        std::vector<Node> conf;
+        conf.push_back(unifEq);
+        Trace("dt-conflict")
+            << "CONFLICT: Clash conflict : " << conf << std::endl;
+        d_im.sendDtConflict(conf, InferenceId::DATATYPES_CLASH_CONFLICT);
+        return;
       }
-
-
-      //merge labels
-      NodeUIntMap::iterator lbl_i = d_labels.find(t2);
-      if( lbl_i != d_labels.end() ){
-        Trace("datatypes-debug") << "  merge labels from " << eqc2 << " " << t2 << std::endl;
-        size_t n_label = (*lbl_i).second;
-        for (size_t i = 0; i < n_label; i++)
+      else
+      {
+        Assert(areEqual(cons1, cons2));
+        // do unification
+        for (size_t i = 0, nchild = cons1.getNumChildren(); i < nchild; i++)
         {
-          Assert(i < d_labels_data[t2].size());
-          Node t = d_labels_data[ t2 ][i];
-          Node t_arg = d_labels_args[t2][i];
-          unsigned tindex = d_labels_tindex[t2][i];
-          addTester( tindex, t, eqc1, t1, t_arg );
-          if (d_state.isInConflict())
+          if (!areEqual(cons1[i], cons2[i]))
           {
-            Trace("datatypes-debug") << "  conflict!" << std::endl;
-            return;
+            Node eq = cons1[i].eqNode(cons2[i]);
+            d_im.addPendingInference(eq, InferenceId::DATATYPES_UNIF, unifEq);
+            Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by "
+                                     << unifEq << std::endl;
           }
         }
-
       }
-      //merge selectors
-      if( !eqc1->d_selectors && eqc2->d_selectors ){
-        eqc1->d_selectors = true;
+    }
+    Trace("datatypes-debug") << "  instantiated : " << eqc1->d_inst << " "
+                             << eqc2->d_inst << std::endl;
+    eqc1->d_inst = eqc1->d_inst || eqc2->d_inst;
+    if (!cons2.isNull())
+    {
+      if (cons1.isNull())
+      {
+        Trace("datatypes-debug")
+            << "  must check if it is okay to set the constructor."
+            << std::endl;
         checkInst = true;
-      }
-      NodeUIntMap::iterator sel_i = d_selector_apps.find(t2);
-      if( sel_i != d_selector_apps.end() ){
-        Trace("datatypes-debug") << "  merge selectors from " << eqc2 << " " << t2 << std::endl;
-        size_t n_sel = (*sel_i).second;
-        for (size_t j = 0; j < n_sel; j++)
-        {
-          addSelector( d_selector_apps_data[t2][j], eqc1, t1, eqc2->d_constructor.get().isNull() );
-        }
-      }
-      if( checkInst ){
-        Trace("datatypes-debug") << "  checking instantiate" << std::endl;
-        instantiate( eqc1, t1 );
+        addConstructor(eqc2->d_constructor.get(), eqc1, t1);
         if (d_state.isInConflict())
         {
           return;
         }
       }
     }
-    Trace("datatypes-debug") << "Finished Merge " << t1 << " " << t2 << std::endl;
   }
+  else
+  {
+    Trace("datatypes-debug")
+        << "  no eqc info for " << t1 << ", must create" << std::endl;
+    // just copy the equivalence class information
+    eqc1 = getOrMakeEqcInfo(t1, true);
+    eqc1->d_inst.set(eqc2->d_inst);
+    eqc1->d_constructor.set(eqc2->d_constructor);
+    eqc1->d_selectors.set(eqc2->d_selectors);
+  }
+
+  // merge labels
+  NodeUIntMap::iterator lbl_i = d_labels.find(t2);
+  if (lbl_i != d_labels.end())
+  {
+    Trace("datatypes-debug")
+        << "  merge labels from " << eqc2 << " " << t2 << std::endl;
+    size_t n_label = (*lbl_i).second;
+    for (size_t i = 0; i < n_label; i++)
+    {
+      Assert(i < d_labels_data[t2].size());
+      Node t = d_labels_data[t2][i];
+      Node t_arg = d_labels_args[t2][i];
+      unsigned tindex = d_labels_tindex[t2][i];
+      addTester(tindex, t, eqc1, t1, t_arg);
+      if (d_state.isInConflict())
+      {
+        Trace("datatypes-debug") << "  conflict!" << std::endl;
+        return;
+      }
+    }
+  }
+  // merge selectors
+  if (!eqc1->d_selectors && eqc2->d_selectors)
+  {
+    eqc1->d_selectors = true;
+    checkInst = true;
+  }
+  NodeUIntMap::iterator sel_i = d_selector_apps.find(t2);
+  if (sel_i != d_selector_apps.end())
+  {
+    Trace("datatypes-debug")
+        << "  merge selectors from " << eqc2 << " " << t2 << std::endl;
+    size_t n_sel = (*sel_i).second;
+    for (size_t j = 0; j < n_sel; j++)
+    {
+      addSelector(d_selector_apps_data[t2][j],
+                  eqc1,
+                  t1,
+                  eqc2->d_constructor.get().isNull());
+    }
+  }
+  if (checkInst)
+  {
+    Trace("datatypes-debug") << "  checking instantiate" << std::endl;
+    instantiate(eqc1, t1);
+  }
+  Trace("datatypes-debug") << "Finished Merge " << t1 << " " << t2 << std::endl;
 }
 
-TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c )
-    : d_inst( c, false )
-    , d_constructor( c, Node::null() )
-    , d_selectors( c, false )
+TheoryDatatypes::EqcInfo::EqcInfo(context::Context* c)
+    : d_inst(c, false),
+      d_constructor(c, Node::null()),
+      d_selectors(c, false)
 {}
 
 bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
@@ -826,7 +844,7 @@ void TheoryDatatypes::addTester(
       const DType& dt = t_arg.getType().getDType();
       Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl;
       if( tpolarity ){
-        instantiate( eqc, n );
+        instantiate(eqc, n);
         // We could propagate is-C1(x) => not is-C2(x) here for all other
         // constructors, but empirically this hurts performance.
       }else{
@@ -1412,13 +1430,14 @@ Node TheoryDatatypes::getInstantiateCons(Node n, const DType& dt, int index)
   return n_ic;
 }
 
-void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
+bool TheoryDatatypes::instantiate(EqcInfo* eqc, Node n)
+{
   Trace("datatypes-debug") << "Instantiate: " << n << std::endl;
   //add constructor to equivalence class if not done so already
   int index = getLabelIndex( eqc, n );
   if (index == -1 || eqc->d_inst)
   {
-    return;
+    return false;
   }
   Node exp;
   Node tt;
@@ -1440,7 +1459,8 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
   Node eq;
   if (tt == tt_cons)
   {
-    return;
+    // not necessary
+    return false;
   }
   eq = tt.eqNode(tt_cons);
   // Determine if the equality must be sent out as a lemma. Notice that
@@ -1463,9 +1483,10 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
   }
   Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq
                                  << " forceLemma = " << forceLemma << std::endl;
-  d_im.addPendingInference(eq, InferenceId::DATATYPES_INST, exp, forceLemma);
   Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp
                            << std::endl;
+  d_im.addPendingInference(eq, InferenceId::DATATYPES_INST, exp, forceLemma);
+  return true;
 }
 
 void TheoryDatatypes::checkCycles() {
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 951aea804..68dedb6f3 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -158,8 +158,6 @@ private:
   std::map< TypeNode, Node > d_singleton_lemma[2];
   /** Cache for singleton equalities processed */
   BoolMap d_singleton_eq;
-  /** list of all lemmas produced */
-  BoolMap d_lemmas_produced_c;
 private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
@@ -183,12 +181,7 @@ private:
   void computeCareGraph() override;
 
  public:
-  TheoryDatatypes(context::Context* c,
-                  context::UserContext* u,
-                  OutputChannel& out,
-                  Valuation valuation,
-                  const LogicInfo& logicInfo,
-                  ProofNodeManager* pnm = nullptr);
+  TheoryDatatypes(Env& env, OutputChannel& out, Valuation valuation);
   ~TheoryDatatypes();
 
   //--------------------------------- initialization
@@ -273,9 +266,10 @@ private:
   void collectTerms( Node n );
   /** get instantiate cons */
   Node getInstantiateCons(Node n, const DType& dt, int index);
-  /** check instantiate */
-  void instantiate( EqcInfo* eqc, Node n );
-private:
+  /** check instantiate, return true if an inference was generated. */
+  bool instantiate(EqcInfo* eqc, Node n);
+
+ private:
   //equality queries
   bool hasTerm( TNode a );
   bool areEqual( TNode a, TNode b );
diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index b4bb896ae..627129c3a 100644
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -84,9 +84,9 @@ bool ExtTheoryCallback::getReduction(int effort,
 ExtTheory::ExtTheory(ExtTheoryCallback& p,
                      context::Context* c,
                      context::UserContext* u,
-                     OutputChannel& out)
+                     TheoryInferenceManager& im)
     : d_parent(p),
-      d_out(out),
+      d_im(im),
       d_ext_func_terms(c),
       d_extfExtReducedIdMap(c),
       d_ci_inactive(u),
@@ -237,7 +237,7 @@ bool ExtTheory::doInferencesInternal(int effort,
           if (!nr.isNull() && n != nr)
           {
             Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, n, nr);
-            if (sendLemma(lem, true))
+            if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY, true))
             {
               Trace("extt-lemma")
                   << "ExtTheory : reduction lemma : " << lem << std::endl;
@@ -287,7 +287,7 @@ bool ExtTheory::doInferencesInternal(int effort,
             Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq
                                 << " by " << exp[i] << std::endl;
             Trace("extt-debug") << "...send lemma " << lem << std::endl;
-            if (sendLemma(lem))
+            if (sendLemma(lem, InferenceId::EXTT_SIMPLIFY))
             {
               Trace("extt-lemma")
                   << "ExtTheory : substitution + rewrite lemma : " << lem
@@ -359,14 +359,14 @@ bool ExtTheory::doInferencesInternal(int effort,
   return false;
 }
 
-bool ExtTheory::sendLemma(Node lem, bool preprocess)
+bool ExtTheory::sendLemma(Node lem, InferenceId id, bool preprocess)
 {
   if (preprocess)
   {
     if (d_pp_lemmas.find(lem) == d_pp_lemmas.end())
     {
       d_pp_lemmas.insert(lem);
-      d_out.lemma(lem);
+      d_im.lemma(lem, id);
       return true;
     }
   }
@@ -375,7 +375,7 @@ bool ExtTheory::sendLemma(Node lem, bool preprocess)
     if (d_lemmas.find(lem) == d_lemmas.end())
     {
       d_lemmas.insert(lem);
-      d_out.lemma(lem);
+      d_im.lemma(lem, id);
       return true;
     }
   }
diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h
index f5e08e2f5..01b191e0a 100644
--- a/src/theory/ext_theory.h
+++ b/src/theory/ext_theory.h
@@ -41,6 +41,7 @@
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "theory/theory_inference_manager.h"
 
 namespace cvc5 {
 namespace theory {
@@ -176,7 +177,7 @@ class ExtTheory
   ExtTheory(ExtTheoryCallback& p,
             context::Context* c,
             context::UserContext* u,
-            OutputChannel& out);
+            TheoryInferenceManager& im);
   virtual ~ExtTheory() {}
   /** Tells this class to treat terms with Kind k as extended functions */
   void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
@@ -291,11 +292,11 @@ class ExtTheory
                             bool batch,
                             bool isRed);
   /** send lemma on the output channel */
-  bool sendLemma(Node lem, bool preprocess = false);
+  bool sendLemma(Node lem, InferenceId id, bool preprocess = false);
   /** reference to the callback */
   ExtTheoryCallback& d_parent;
-  /** Reference to the output channel we are using */
-  OutputChannel& d_out;
+  /** inference manager used to send lemmas */
+  TheoryInferenceManager& d_im;
   /** the true node */
   Node d_true;
   /** extended function terms, map to whether they are active */
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 9b5ac66d3..bd5662cdd 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -60,24 +60,19 @@ Node buildConjunct(const std::vector<TNode> &assumptions) {
 }  // namespace helper
 
 /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-TheoryFp::TheoryFp(context::Context* c,
-                   context::UserContext* u,
-                   OutputChannel& out,
-                   Valuation valuation,
-                   const LogicInfo& logicInfo,
-                   ProofNodeManager* pnm)
-    : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm),
+TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation)
+    : Theory(THEORY_FP, env, out, valuation),
       d_notification(*this),
-      d_registeredTerms(u),
-      d_conv(new FpConverter(u)),
+      d_registeredTerms(getUserContext()),
+      d_conv(new FpConverter(getUserContext())),
       d_expansionRequested(false),
-      d_realToFloatMap(u),
-      d_floatToRealMap(u),
-      d_abstractionMap(u),
-      d_rewriter(u),
-      d_state(c, u, valuation),
-      d_im(*this, d_state, pnm, "theory::fp::", false),
-      d_wbFactsCache(u)
+      d_realToFloatMap(getUserContext()),
+      d_floatToRealMap(getUserContext()),
+      d_abstractionMap(getUserContext()),
+      d_rewriter(getUserContext()),
+      d_state(env, valuation),
+      d_im(*this, d_state, d_pnm, "theory::fp::", false),
+      d_wbFactsCache(getUserContext())
 {
   // indicate we are using the default theory state and inference manager
   d_theoryState = &d_state;
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 14779cc3d..1e1041980 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -39,12 +39,7 @@ class TheoryFp : public Theory
 {
  public:
   /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-  TheoryFp(context::Context* c,
-           context::UserContext* u,
-           OutputChannel& out,
-           Valuation valuation,
-           const LogicInfo& logicInfo,
-           ProofNodeManager* pnm = nullptr);
+  TheoryFp(Env& env, OutputChannel& out, Valuation valuation);
 
   //--------------------------------- initialization
   /** Get the official theory rewriter of this theory. */
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 9d8cddb69..7bb87819e 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -28,6 +28,7 @@ const char* toString(InferenceId i)
   {
     case InferenceId::EQ_CONSTANT_MERGE: return "EQ_CONSTANT_MERGE";
     case InferenceId::COMBINATION_SPLIT: return "COMBINATION_SPLIT";
+    case InferenceId::EXTT_SIMPLIFY: return "EXTT_SIMPLIFY";
     case InferenceId::ARITH_BLACK_BOX: return "ARITH_BLACK_BOX";
     case InferenceId::ARITH_CONF_EQ: return "ARITH_CONF_EQ";
     case InferenceId::ARITH_CONF_LOWER: return "ARITH_CONF_LOWER";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 3a317e0a4..4c6140872 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -45,6 +45,9 @@ enum class InferenceId
   EQ_CONSTANT_MERGE,
   // a split from theory combination
   COMBINATION_SPLIT,
+  // ---------------------------------- ext theory
+  // a simplification from the extended theory utility
+  EXTT_SIMPLIFY,
   // ---------------------------------- arith theory
   //-------------------- linear core
   // black box conflicts. It's magic.
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index ab237fc6c..8901ec314 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -111,7 +111,10 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
                                                         int e)
 {
   options::UserPatMode upMode = getInstUserPatMode();
-  if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST)
+  // we don't auto-generate triggers if the mode is trust or strict
+  if (hasUserPatterns(f)
+      && (upMode == options::UserPatMode::TRUST
+          || upMode == options::UserPatMode::STRICT))
   {
     return InstStrategyStatus::STATUS_UNKNOWN;
   }
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index d490dce83..d9bec820c 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -200,11 +200,15 @@ bool InstantiationEngine::checkCompleteFor( Node q ) {
 
 void InstantiationEngine::checkOwnership(Node q)
 {
-  if( options::strictTriggers() && q.getNumChildren()==3 ){
+  if (options::userPatternsQuant() == options::UserPatMode::STRICT
+      && q.getNumChildren() == 3)
+  {
     //if strict triggers, take ownership of this quantified formula
     bool hasPat = false;
-    for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
-      if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN  ){
+    for (const Node& qc : q)
+    {
+      if (qc.getKind() == INST_PATTERN || qc.getKind() == INST_NO_PATTERN)
+      {
         hasPat = true;
         break;
       }
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 72605e9d1..0f46fa790 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -38,38 +38,19 @@ void ExprMiner::initialize(const std::vector<Node>& vars, SygusSampler* ss)
 
 Node ExprMiner::convertToSkolem(Node n)
 {
-  std::vector<Node> fvs;
-  TermUtil::computeVarContains(n, fvs);
-  if (fvs.empty())
+  if (d_skolems.empty())
   {
-    return n;
-  }
-  std::vector<Node> sfvs;
-  std::vector<Node> sks;
-  // map to skolems
-  NodeManager* nm = NodeManager::currentNM();
-  SkolemManager* sm = nm->getSkolemManager();
-  for (unsigned i = 0, size = fvs.size(); i < size; i++)
-  {
-    Node v = fvs[i];
-    // only look at the sampler variables
-    if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end())
+    NodeManager* nm = NodeManager::currentNM();
+    SkolemManager* sm = nm->getSkolemManager();
+    for (const Node& v : d_vars)
     {
-      sfvs.push_back(v);
-      std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
-      if (itf == d_fv_to_skolem.end())
-      {
-        Node sk = sm->mkDummySkolem("rrck", v.getType());
-        d_fv_to_skolem[v] = sk;
-        sks.push_back(sk);
-      }
-      else
-      {
-        sks.push_back(itf->second);
-      }
+      Node sk = sm->mkDummySkolem("rrck", v.getType());
+      d_skolems.push_back(sk);
+      d_fv_to_skolem[v] = sk;
     }
   }
-  return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
+  return n.substitute(
+      d_vars.begin(), d_vars.end(), d_skolems.begin(), d_skolems.end());
 }
 
 void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index 36fae1549..79d0c6650 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -62,13 +62,15 @@ class ExprMiner
  protected:
   /** the set of variables used by this class */
   std::vector<Node> d_vars;
-  /** pointer to the sygus sampler object we are using */
-  SygusSampler* d_sampler;
   /**
-   * Maps to skolems for each free variable that appears in a check. This is
+   * The set of skolems corresponding to the above variables. These are
    * used during initializeChecker so that query (which may contain free
    * variables) is converted to a formula without free variables.
    */
+  std::vector<Node> d_skolems;
+  /** pointer to the sygus sampler object we are using */
+  SygusSampler* d_sampler;
+  /** Maps to skolems for each free variable based on d_vars/d_skolems. */
   std::map<Node, Node> d_fv_to_skolem;
   /** convert */
   Node convertToSkolem(Node n);
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 1abbd1989..33ed6f536 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -30,8 +30,7 @@ namespace quantifiers {
 
 bool QAttributes::isStandard() const
 {
-  return !d_sygus && !d_quant_elim && !isFunDef() && d_name.isNull()
-         && !d_isInternal;
+  return !d_sygus && !d_quant_elim && !isFunDef() && !d_isInternal;
 }
 
 QuantAttributes::QuantAttributes() {}
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index b3fdd09da..910dbab5b 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -162,8 +162,7 @@ struct QAttributes
    * perform destructive updates (variable elimination, miniscoping, etc).
    *
    * A quantified formula is not standard if it is sygus, one for which
-   * we are performing quantifier elimination, is a function definition, or
-   * has a name.
+   * we are performing quantifier elimination, or is a function definition.
    */
   bool isStandard() const;
 };
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 48106b858..02af92887 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -701,9 +701,65 @@ bool QuantifiersRewriter::isVarElim(Node v, Node s)
   return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType());
 }
 
-Node QuantifiersRewriter::getVarElimLitBv(Node lit,
-                                          const std::vector<Node>& args,
-                                          Node& var)
+Node QuantifiersRewriter::getVarElimEq(Node lit,
+                                       const std::vector<Node>& args,
+                                       Node& var)
+{
+  Assert(lit.getKind() == EQUAL);
+  Node slv;
+  TypeNode tt = lit[0].getType();
+  if (tt.isReal())
+  {
+    slv = getVarElimEqReal(lit, args, var);
+  }
+  else if (tt.isBitVector())
+  {
+    slv = getVarElimEqBv(lit, args, var);
+  }
+  else if (tt.isStringLike())
+  {
+    slv = getVarElimEqString(lit, args, var);
+  }
+  return slv;
+}
+
+Node QuantifiersRewriter::getVarElimEqReal(Node lit,
+                                           const std::vector<Node>& args,
+                                           Node& var)
+{
+  // for arithmetic, solve the equality
+  std::map<Node, Node> msum;
+  if (!ArithMSum::getMonomialSumLit(lit, msum))
+  {
+    return Node::null();
+  }
+  std::vector<Node>::const_iterator ita;
+  for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end();
+       ++itm)
+  {
+    if (itm->first.isNull())
+    {
+      continue;
+    }
+    ita = std::find(args.begin(), args.end(), itm->first);
+    if (ita != args.end())
+    {
+      Node veq_c;
+      Node val;
+      int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL);
+      if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val))
+      {
+        var = itm->first;
+        return val;
+      }
+    }
+  }
+  return Node::null();
+}
+
+Node QuantifiersRewriter::getVarElimEqBv(Node lit,
+                                         const std::vector<Node>& args,
+                                         Node& var)
 {
   if (Trace.isOn("quant-velim-bv"))
   {
@@ -752,9 +808,9 @@ Node QuantifiersRewriter::getVarElimLitBv(Node lit,
   return Node::null();
 }
 
-Node QuantifiersRewriter::getVarElimLitString(Node lit,
-                                              const std::vector<Node>& args,
-                                              Node& var)
+Node QuantifiersRewriter::getVarElimEqString(Node lit,
+                                             const std::vector<Node>& args,
+                                             Node& var)
 {
   Assert(lit.getKind() == EQUAL);
   NodeManager* nm = NodeManager::currentNM();
@@ -900,48 +956,10 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
       return true;
     }
   }
-  if (lit.getKind() == EQUAL && lit[0].getType().isReal() && pol)
-  {
-    // for arithmetic, solve the equality
-    std::map< Node, Node > msum;
-    if (ArithMSum::getMonomialSumLit(lit, msum))
-    {
-      for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
-        if( !itm->first.isNull() ){
-          std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first );
-          if( ita!=args.end() ){
-            Assert(pol);
-            Node veq_c;
-            Node val;
-            int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL);
-            if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val))
-            {
-              Trace("var-elim-quant")
-                  << "Variable eliminate based on solved equality : "
-                  << itm->first << " -> " << val << std::endl;
-              vars.push_back(itm->first);
-              subs.push_back(val);
-              args.erase(ita);
-              return true;
-            }
-          }
-        }
-      }
-    }
-  }
   if (lit.getKind() == EQUAL && pol)
   {
     Node var;
-    Node slv;
-    TypeNode tt = lit[0].getType();
-    if (tt.isBitVector())
-    {
-      slv = getVarElimLitBv(lit, args, var);
-    }
-    else if (tt.isStringLike())
-    {
-      slv = getVarElimLitString(lit, args, var);
-    }
+    Node slv = getVarElimEq(lit, args, var);
     if (!slv.isNull())
     {
       Assert(!var.isNull());
@@ -1797,7 +1815,7 @@ bool QuantifiersRewriter::doOperation(Node q,
 {
   bool is_strict_trigger =
       qa.d_hasPattern
-      && options::userPatternsQuant() == options::UserPatMode::TRUST;
+      && options::userPatternsQuant() == options::UserPatMode::STRICT;
   bool is_std = qa.isStandard() && !is_strict_trigger;
   if (computeOption == COMPUTE_ELIM_SYMBOLS)
   {
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index ae7f75f34..f0c3b0414 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -80,22 +80,34 @@ class QuantifiersRewriter : public TheoryRewriter
                             std::vector<Node>& args,
                             std::vector<Node>& vars,
                             std::vector<Node>& subs);
+  /**
+   * Get variable eliminate for an equality based on theory-specific reasoning.
+   */
+  static Node getVarElimEq(Node lit, const std::vector<Node>& args, Node& var);
+  /** variable eliminate for real equalities
+   *
+   * If this returns a non-null value ret, then var is updated to a member of
+   * args, lit is equivalent to ( var = ret ).
+   */
+  static Node getVarElimEqReal(Node lit,
+                               const std::vector<Node>& args,
+                               Node& var);
   /** variable eliminate for bit-vector equalities
    *
    * If this returns a non-null value ret, then var is updated to a member of
    * args, lit is equivalent to ( var = ret ).
    */
-  static Node getVarElimLitBv(Node lit,
-                              const std::vector<Node>& args,
-                              Node& var);
+  static Node getVarElimEqBv(Node lit,
+                             const std::vector<Node>& args,
+                             Node& var);
   /** variable eliminate for string equalities
    *
    * If this returns a non-null value ret, then var is updated to a member of
    * args, lit is equivalent to ( var = ret ).
    */
-  static Node getVarElimLitString(Node lit,
-                                  const std::vector<Node>& args,
-                                  Node& var);
+  static Node getVarElimEqString(Node lit,
+                                 const std::vector<Node>& args,
+                                 Node& var);
   /** get variable elimination
    *
    * If n asserted with polarity pol entails a literal lit that corresponds
diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
index 7654a6326..39af9c2c9 100644
--- a/src/theory/quantifiers/quantifiers_state.cpp
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -22,11 +22,12 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-QuantifiersState::QuantifiersState(context::Context* c,
-                                   context::UserContext* u,
+QuantifiersState::QuantifiersState(Env& env,
                                    Valuation val,
                                    const LogicInfo& logicInfo)
-    : TheoryState(c, u, val), d_ierCounterc(c), d_logicInfo(logicInfo)
+    : TheoryState(env, val),
+      d_ierCounterc(env.getContext()),
+      d_logicInfo(logicInfo)
 {
   // allow theory combination to go first, once initially
   d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h
index e4a05b078..92b744cd0 100644
--- a/src/theory/quantifiers/quantifiers_state.h
+++ b/src/theory/quantifiers/quantifiers_state.h
@@ -32,8 +32,7 @@ namespace quantifiers {
 class QuantifiersState : public TheoryState
 {
  public:
-  QuantifiersState(context::Context* c,
-                   context::UserContext* u,
+  QuantifiersState(Env& env,
                    Valuation val,
                    const LogicInfo& logicInfo);
   ~QuantifiersState() {}
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index c74146c9c..a108d4614 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -30,17 +30,14 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-TheoryQuantifiers::TheoryQuantifiers(Context* c,
-                                     context::UserContext* u,
+TheoryQuantifiers::TheoryQuantifiers(Env& env,
                                      OutputChannel& out,
-                                     Valuation valuation,
-                                     const LogicInfo& logicInfo,
-                                     ProofNodeManager* pnm)
-    : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm),
-      d_qstate(c, u, valuation, logicInfo),
+                                     Valuation valuation)
+    : Theory(THEORY_QUANTIFIERS, env, out, valuation),
+      d_qstate(env, valuation, getLogicInfo()),
       d_qreg(),
       d_treg(d_qstate, d_qreg),
-      d_qim(*this, d_qstate, d_qreg, d_treg, pnm),
+      d_qim(*this, d_qstate, d_qreg, d_treg, d_pnm),
       d_qengine(nullptr)
 {
   out.handleUserAttribute( "fun-def", this );
@@ -50,7 +47,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
   out.handleUserAttribute( "quant-elim-partial", this );
 
   // construct the quantifiers engine
-  d_qengine.reset(new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, pnm));
+  d_qengine.reset(
+      new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, d_pnm));
 
   // indicate we are using the quantifiers theory state object
   d_theoryState = &d_qstate;
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 544be84d6..0ef5cfcbb 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -37,12 +37,7 @@ class QuantifiersMacros;
 
 class TheoryQuantifiers : public Theory {
  public:
-  TheoryQuantifiers(context::Context* c,
-                    context::UserContext* u,
-                    OutputChannel& out,
-                    Valuation valuation,
-                    const LogicInfo& logicInfo,
-                    ProofNodeManager* pnm = nullptr);
+  TheoryQuantifiers(Env& env, OutputChannel& out, Valuation valuation);
   ~TheoryQuantifiers();
 
   //--------------------------------- initialization
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 98130beb5..92d15653e 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -42,20 +42,15 @@ namespace cvc5 {
 namespace theory {
 namespace sep {
 
-TheorySep::TheorySep(context::Context* c,
-                     context::UserContext* u,
-                     OutputChannel& out,
-                     Valuation valuation,
-                     const LogicInfo& logicInfo,
-                     ProofNodeManager* pnm)
-    : Theory(THEORY_SEP, c, u, out, valuation, logicInfo, pnm),
-      d_lemmas_produced_c(u),
+TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation)
+    : Theory(THEORY_SEP, env, out, valuation),
+      d_lemmas_produced_c(getUserContext()),
       d_bounds_init(false),
-      d_state(c, u, valuation),
-      d_im(*this, d_state, pnm, "theory::sep::"),
+      d_state(env, valuation),
+      d_im(*this, d_state, d_pnm, "theory::sep::"),
       d_notify(*this),
-      d_reduce(u),
-      d_spatial_assertions(c)
+      d_reduce(getUserContext()),
+      d_spatial_assertions(getSatContext())
 {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index b028f0686..985513fd8 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -77,12 +77,7 @@ class TheorySep : public Theory {
       bool underSpatial);
 
  public:
-  TheorySep(context::Context* c,
-            context::UserContext* u,
-            OutputChannel& out,
-            Valuation valuation,
-            const LogicInfo& logicInfo,
-            ProofNodeManager* pnm = nullptr);
+  TheorySep(Env& env, OutputChannel& out, Valuation valuation);
   ~TheorySep();
 
   /**
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 2aaa82706..6f8976f4d 100644
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -26,11 +26,8 @@ namespace cvc5 {
 namespace theory {
 namespace sets {
 
-SolverState::SolverState(context::Context* c,
-                         context::UserContext* u,
-                         Valuation val,
-                         SkolemCache& skc)
-    : TheoryState(c, u, val), d_skCache(skc), d_members(c)
+SolverState::SolverState(Env& env, Valuation val, SkolemCache& skc)
+    : TheoryState(env, val), d_skCache(skc), d_members(env.getContext())
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h
index 63039eddd..ff9bc8bf9 100644
--- a/src/theory/sets/solver_state.h
+++ b/src/theory/sets/solver_state.h
@@ -46,8 +46,7 @@ class SolverState : public TheoryState
   typedef context::CDHashMap<Node, size_t> NodeIntMap;
 
  public:
-  SolverState(context::Context* c,
-              context::UserContext* u,
+  SolverState(Env& env,
               Valuation val,
               SkolemCache& skc);
   //-------------------------------- initialize per check
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 718077888..23ac08749 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -27,17 +27,12 @@ namespace cvc5 {
 namespace theory {
 namespace sets {
 
-TheorySets::TheorySets(context::Context* c,
-                       context::UserContext* u,
-                       OutputChannel& out,
-                       Valuation valuation,
-                       const LogicInfo& logicInfo,
-                       ProofNodeManager* pnm)
-    : Theory(THEORY_SETS, c, u, out, valuation, logicInfo, pnm),
+TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation)
+    : Theory(THEORY_SETS, env, out, valuation),
       d_skCache(),
-      d_state(c, u, valuation, d_skCache),
-      d_im(*this, d_state, pnm),
-      d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, pnm)),
+      d_state(env, valuation, d_skCache),
+      d_im(*this, d_state, d_pnm),
+      d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, d_pnm)),
       d_notify(*d_internal.get(), d_im)
 {
   // use the official theory state and inference manager objects
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index e99d25d36..e9510d70e 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -41,12 +41,7 @@ class TheorySets : public Theory
   friend class TheorySetsRels;
  public:
   /** Constructs a new instance of TheorySets w.r.t. the provided contexts. */
-  TheorySets(context::Context* c,
-             context::UserContext* u,
-             OutputChannel& out,
-             Valuation valuation,
-             const LogicInfo& logicInfo,
-             ProofNodeManager* pnm);
+  TheorySets(Env& env, OutputChannel& out, Valuation valuation);
   ~TheorySets() override;
 
   //--------------------------------- initialization
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index 432aa39d0..aabefe74e 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/strings/inference_manager.h"
 #include "theory/strings/theory_strings_utils.h"
+#include "theory/theory.h"
 
 namespace cvc5 {
 namespace theory {
@@ -60,8 +61,8 @@ bool InferInfo::isFact() const
   // we could process inferences with conjunctive conclusions as facts, where
   // the explanation is copied. However, for simplicity, we always send these
   // as lemmas. This case happens very infrequently.
-  return !atom.isConst() && atom.getKind() != kind::OR
-         && atom.getKind() != kind::AND && d_noExplain.empty();
+  return !atom.isConst() && Theory::theoryOf(atom) == THEORY_STRINGS
+         && d_noExplain.empty();
 }
 
 Node InferInfo::getPremises() const
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 1ddf2af58..32ed6896c 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -28,10 +28,11 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-SolverState::SolverState(context::Context* c,
-                         context::UserContext* u,
-                         Valuation& v)
-    : TheoryState(c, u, v), d_eeDisequalities(c), d_pendingConflictSet(c, false), d_pendingConflict(InferenceId::UNKNOWN)
+SolverState::SolverState(Env& env, Valuation& v)
+    : TheoryState(env, v),
+      d_eeDisequalities(env.getContext()),
+      d_pendingConflictSet(env.getContext(), false),
+      d_pendingConflict(InferenceId::UNKNOWN)
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -64,7 +65,7 @@ EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake)
   }
   if (doMake)
   {
-    EqcInfo* ei = new EqcInfo(d_context);
+    EqcInfo* ei = new EqcInfo(d_env.getContext());
     d_eqcInfo[eqc] = ei;
     return ei;
   }
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index 422c29760..bbeb470f7 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -48,8 +48,7 @@ class SolverState : public TheoryState
   typedef context::CDList<Node> NodeList;
 
  public:
-  SolverState(context::Context* c,
-              context::UserContext* u,
+  SolverState(Env& env,
               Valuation& v);
   ~SolverState();
   //-------------------------------------- disequality information
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index c526decf1..8b71df31b 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -50,21 +50,16 @@ struct SeqModelVarAttributeId
 };
 using SeqModelVarAttribute = expr::Attribute<SeqModelVarAttributeId, Node>;
 
-TheoryStrings::TheoryStrings(context::Context* c,
-                             context::UserContext* u,
-                             OutputChannel& out,
-                             Valuation valuation,
-                             const LogicInfo& logicInfo,
-                             ProofNodeManager* pnm)
-    : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, pnm),
+TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
+    : Theory(THEORY_STRINGS, env, out, valuation),
       d_notify(*this),
       d_statistics(),
-      d_state(c, u, d_valuation),
+      d_state(env, d_valuation),
       d_eagerSolver(d_state),
-      d_termReg(d_state, d_statistics, pnm),
+      d_termReg(d_state, d_statistics, d_pnm),
       d_extTheoryCb(),
-      d_extTheory(d_extTheoryCb, c, u, out),
-      d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, pnm),
+      d_im(*this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm),
+      d_extTheory(d_extTheoryCb, getSatContext(), getUserContext(), d_im),
       d_rewriter(&d_statistics.d_rewrites),
       d_bsolver(d_state, d_im),
       d_csolver(d_state, d_im, d_termReg, d_bsolver),
@@ -82,8 +77,8 @@ TheoryStrings::TheoryStrings(context::Context* c,
                 d_csolver,
                 d_esolver,
                 d_statistics),
-      d_regexp_elim(options::regExpElimAgg(), pnm, u),
-      d_stringsFmf(c, u, valuation, d_termReg)
+      d_regexp_elim(options::regExpElimAgg(), d_pnm, getUserContext()),
+      d_stringsFmf(getSatContext(), getUserContext(), valuation, d_termReg)
 {
   d_termReg.finishInit(&d_im);
 
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index fc5e47194..8f0205b48 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -64,12 +64,7 @@ class TheoryStrings : public Theory {
   typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet;
 
  public:
-  TheoryStrings(context::Context* c,
-                context::UserContext* u,
-                OutputChannel& out,
-                Valuation valuation,
-                const LogicInfo& logicInfo,
-                ProofNodeManager* pnm);
+  TheoryStrings(Env& env, OutputChannel& out, Valuation valuation);
   ~TheoryStrings();
   //--------------------------------- initialization
   /** get the official theory rewriter of this theory */
@@ -267,10 +262,10 @@ class TheoryStrings : public Theory {
   TermRegistry d_termReg;
   /** The extended theory callback */
   StringsExtfCallback d_extTheoryCb;
-  /** Extended theory, responsible for context-dependent simplification. */
-  ExtTheory d_extTheory;
   /** The (custom) output channel of the theory of strings */
   InferenceManager d_im;
+  /** Extended theory, responsible for context-dependent simplification. */
+  ExtTheory d_extTheory;
   /** The theory rewriter for this theory. */
   StringsRewriter d_rewriter;
   /** The proof rule checker */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 96bc85336..04bab16e2 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -60,27 +60,22 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){
 }/* ostream& operator<<(ostream&, Theory::Effort) */
 
 Theory::Theory(TheoryId id,
-               context::Context* satContext,
-               context::UserContext* userContext,
+               Env& env,
                OutputChannel& out,
                Valuation valuation,
-               const LogicInfo& logicInfo,
-               ProofNodeManager* pnm,
                std::string name)
     : d_id(id),
-      d_satContext(satContext),
-      d_userContext(userContext),
-      d_logicInfo(logicInfo),
-      d_facts(satContext),
-      d_factsHead(satContext, 0),
-      d_sharedTermsIndex(satContext, 0),
+      d_env(env),
+      d_facts(d_env.getContext()),
+      d_factsHead(d_env.getContext(), 0),
+      d_sharedTermsIndex(d_env.getContext(), 0),
       d_careGraph(nullptr),
       d_instanceName(name),
       d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id)
                                                         + name + "checkTime")),
       d_computeCareGraphTime(smtStatisticsRegistry().registerTimer(
           getStatsPrefix(id) + name + "computeCareGraphTime")),
-      d_sharedTerms(satContext),
+      d_sharedTerms(d_env.getContext()),
       d_out(&out),
       d_valuation(valuation),
       d_equalityEngine(nullptr),
@@ -88,7 +83,8 @@ Theory::Theory(TheoryId id,
       d_theoryState(nullptr),
       d_inferManager(nullptr),
       d_quantEngine(nullptr),
-      d_pnm(pnm)
+      d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
+                                           : nullptr)
 {
 }
 
@@ -135,9 +131,12 @@ void Theory::finishInitStandalone()
   EeSetupInfo esi;
   if (needsEqualityEngine(esi))
   {
-    // always associated with the same SAT context as the theory (d_satContext)
-    d_allocEqualityEngine.reset(new eq::EqualityEngine(
-        *esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers));
+    // always associated with the same SAT context as the theory
+    d_allocEqualityEngine.reset(
+        new eq::EqualityEngine(*esi.d_notify,
+                               getSatContext(),
+                               esi.d_name,
+                               esi.d_constantsAreTriggers));
     // use it as the official equality engine
     setEqualityEngine(d_allocEqualityEngine.get());
   }
@@ -339,7 +338,7 @@ bool Theory::isLegalElimination(TNode x, TNode val)
   {
     return false;
   }
-  if (!options::produceModels() && !d_logicInfo.isQuantified())
+  if (!options::produceModels() && !getLogicInfo().isQuantified())
   {
     // Don't care about the model and logic is not quantified, we can eliminate.
     return true;
@@ -467,7 +466,7 @@ void Theory::getCareGraph(CareGraph* careGraph) {
 
 bool Theory::proofsEnabled() const
 {
-  return d_pnm != nullptr;
+  return d_env.getProofNodeManager() != nullptr;
 }
 
 EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
@@ -621,7 +620,7 @@ bool Theory::usesCentralEqualityEngine(TheoryId id)
   }
   return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS
          || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS
-         || id == THEORY_SEP || id == THEORY_ARRAYS;
+         || id == THEORY_SEP || id == THEORY_ARRAYS || id == THEORY_BV;
 }
 
 bool Theory::expUsingCentralEqualityEngine(TheoryId id)
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 41f35601b..a857931a8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -29,6 +29,7 @@
 #include "expr/node.h"
 #include "options/theory_options.h"
 #include "proof/trust_node.h"
+#include "smt/env.h"
 #include "theory/assertion.h"
 #include "theory/care_graph.h"
 #include "theory/logic_info.h"
@@ -105,14 +106,8 @@ class Theory {
   /** An integer identifying the type of the theory. */
   TheoryId d_id;
 
-  /** The SAT search context for the Theory. */
-  context::Context* d_satContext;
-
-  /** The user level assertion context for the Theory. */
-  context::UserContext* d_userContext;
-
-  /** Information about the logic we're operating within. */
-  const LogicInfo& d_logicInfo;
+  /** The environment class */
+  Env& d_env;
 
   /**
    * The assertFact() queue.
@@ -169,12 +164,9 @@ class Theory {
    * w.r.t. the SmtEngine.
    */
   Theory(TheoryId id,
-         context::Context* satContext,
-         context::UserContext* userContext,
+         Env& env,
          OutputChannel& out,
          Valuation valuation,
-         const LogicInfo& logicInfo,
-         ProofNodeManager* pnm,
          std::string instance = "");  // taking : No default.
 
   /**
@@ -241,9 +233,7 @@ class Theory {
    */
   inline Assertion get();
 
-  const LogicInfo& getLogicInfo() const {
-    return d_logicInfo;
-  }
+  const LogicInfo& getLogicInfo() const { return d_env.getLogicInfo(); }
 
   /**
    * Set separation logic heap. This is called when the location and data
@@ -455,17 +445,20 @@ class Theory {
   }
 
   /**
+   * Get a reference to the environment.
+   */
+  Env& getEnv() const { return d_env; }
+
+  /**
    * Get the SAT context associated to this Theory.
    */
-  context::Context* getSatContext() const {
-    return d_satContext;
-  }
+  context::Context* getSatContext() const { return d_env.getContext(); }
 
   /**
    * Get the context associated to this Theory.
    */
   context::UserContext* getUserContext() const {
-    return d_userContext;
+    return d_env.getUserContext();
   }
 
   /**
@@ -512,7 +505,7 @@ class Theory {
    */
   void assertFact(TNode assertion, bool isPreregistered) {
     Trace("theory") << "Theory<" << getId() << ">::assertFact["
-                    << d_satContext->getLevel() << "](" << assertion << ", "
+                    << getSatContext()->getLevel() << "](" << assertion << ", "
                     << (isPreregistered ? "true" : "false") << ")" << std::endl;
     d_facts.push_back(Assertion(assertion, isPreregistered));
   }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 233ea64ed..21c22586b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -218,12 +218,12 @@ context::UserContext* TheoryEngine::getUserContext() const
   return d_env.getUserContext();
 }
 
-TheoryEngine::TheoryEngine(Env& env,
-                           ProofNodeManager* pnm)
+TheoryEngine::TheoryEngine(Env& env)
     : d_propEngine(nullptr),
       d_env(env),
       d_logicInfo(env.getLogicInfo()),
-      d_pnm(pnm),
+      d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
+                                           : nullptr),
       d_lazyProof(d_pnm != nullptr
                       ? new LazyCDProof(d_pnm,
                                         nullptr,
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0c4a80c98..1c42e336f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -295,7 +295,7 @@ class TheoryEngine {
 
  public:
   /** Constructs a theory engine */
-  TheoryEngine(Env& env, ProofNodeManager* pnm);
+  TheoryEngine(Env& env);
 
   /** Destroys a theory engine */
   ~TheoryEngine();
@@ -314,12 +314,8 @@ class TheoryEngine {
   {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
     d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId);
-    d_theoryTable[theoryId] = new TheoryClass(getSatContext(),
-                                              getUserContext(),
-                                              *d_theoryOut[theoryId],
-                                              theory::Valuation(this),
-                                              d_logicInfo,
-                                              d_pnm);
+    d_theoryTable[theoryId] =
+        new TheoryClass(d_env, *d_theoryOut[theoryId], theory::Valuation(this));
     theory::Rewriter::registerTheoryRewriter(
         theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
   }
diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index 5ac5e6ae9..72ab24a7e 100644
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -20,22 +20,25 @@
 namespace cvc5 {
 namespace theory {
 
-TheoryState::TheoryState(context::Context* c,
-                         context::UserContext* u,
-                         Valuation val)
-    : d_context(c),
-      d_ucontext(u),
+TheoryState::TheoryState(Env& env, Valuation val)
+    : d_env(env),
       d_valuation(val),
       d_ee(nullptr),
-      d_conflict(c, false)
+      d_conflict(d_env.getContext(), false)
 {
 }
 
 void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
 
-context::Context* TheoryState::getSatContext() const { return d_context; }
+context::Context* TheoryState::getSatContext() const
+{
+  return d_env.getContext();
+}
 
-context::UserContext* TheoryState::getUserContext() const { return d_ucontext; }
+context::UserContext* TheoryState::getUserContext() const
+{
+  return d_env.getUserContext();
+}
 
 bool TheoryState::hasTerm(TNode a) const
 {
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 2c7bad60b..58a66ef46 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -20,6 +20,7 @@
 
 #include "context/cdo.h"
 #include "expr/node.h"
+#include "smt/env.h"
 #include "theory/valuation.h"
 
 namespace cvc5 {
@@ -32,7 +33,8 @@ class EqualityEngine;
 class TheoryState
 {
  public:
-  TheoryState(context::Context* c, context::UserContext* u, Valuation val);
+  TheoryState(Env& env,
+              Valuation val);
   virtual ~TheoryState() {}
   /**
    * Set equality engine, where ee is a pointer to the official equality engine
@@ -43,6 +45,8 @@ class TheoryState
   context::Context* getSatContext() const;
   /** Get the user context */
   context::UserContext* getUserContext() const;
+  /** Get the environment */
+  Env& getEnv() const { return d_env; }
   //-------------------------------------- equality information
   /** Is t registered as a term in the equality engine of this class? */
   virtual bool hasTerm(TNode a) const;
@@ -111,10 +115,8 @@ class TheoryState
   Valuation& getValuation();
 
  protected:
-  /** Pointer to the SAT context object used by the theory. */
-  context::Context* d_context;
-  /** Pointer to the user context object used by the theory. */
-  context::UserContext* d_ucontext;
+  /** Reference to the environment. */
+  Env& d_env;
   /**
    * The valuation proxy for the Theory to communicate back with the
    * theory engine (and other theories).
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 4224ec854..3525786d5 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -40,20 +40,17 @@ namespace theory {
 namespace uf {
 
 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-TheoryUF::TheoryUF(context::Context* c,
-                   context::UserContext* u,
+TheoryUF::TheoryUF(Env& env,
                    OutputChannel& out,
                    Valuation valuation,
-                   const LogicInfo& logicInfo,
-                   ProofNodeManager* pnm,
                    std::string instanceName)
-    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, pnm, instanceName),
+    : Theory(THEORY_UF, env, out, valuation, instanceName),
       d_thss(nullptr),
       d_ho(nullptr),
-      d_functionsTerms(c),
-      d_symb(u, instanceName),
-      d_state(c, u, valuation),
-      d_im(*this, d_state, pnm, "theory::uf::" + instanceName, false),
+      d_functionsTerms(getSatContext()),
+      d_symb(getUserContext(), instanceName),
+      d_state(env, valuation),
+      d_im(*this, d_state, d_pnm, "theory::uf::" + instanceName, false),
       d_notify(d_im, *this)
 {
   d_true = NodeManager::currentNM()->mkConst( true );
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index c953cfe5c..6f04035ed 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -98,12 +98,9 @@ private:
  public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(context::Context* c,
-           context::UserContext* u,
+  TheoryUF(Env& env,
            OutputChannel& out,
            Valuation valuation,
-           const LogicInfo& logicInfo,
-           ProofNodeManager* pnm = nullptr,
            std::string instanceName = "");
 
   ~TheoryUF();