Merge branch 'master' into rmNoInteractivePromptrmNoInteractivePrompt

76 files changed, 903 insertions, 841 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index bc7103f0d..2aa91f61b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -323,6 +323,8 @@ libcvc5_add_sources(
   smt/process_assertions.h
   smt/proof_manager.cpp
   smt/proof_manager.h
+  smt/proof_final_callback.cpp
+  smt/proof_final_callback.h
   smt/proof_post_processor.cpp
   smt/proof_post_processor.h
   smt/set_defaults.cpp
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index edc0f88f4..a861b06eb 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -610,12 +610,20 @@ def codegen_module(module, dst_dir, tpls):
                     cases=''.join(cases)))
 
             # Generate str-to-enum handler
+            names = set()
             cases = []
             for value, attrib in option.mode.items():
                 assert len(attrib) == 1
+                name = attrib[0]['name']
+                if name in names:
+                    die("multiple modes with the name '{}' for option '{}'".
+                        format(name, option.long))
+                else:
+                    names.add(name)
+
                 cases.append(
                     TPL_MODE_HANDLER_CASE.format(
-                        name=attrib[0]['name'],
+                        name=name,
                         type=option.type,
                         enum=value))
             assert option.long
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 55661a094..42a63b47c 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -209,34 +209,6 @@ void OptionsHandler::setBitblastAig(const std::string& option,
   }
 }
 
-// printer/options_handlers.h
-const std::string OptionsHandler::s_instFormatHelp = "\
-Inst format modes currently supported by the --inst-format option:\n\
-\n\
-default \n\
-+ Print instantiations as a list in the output language format.\n\
-\n\
-szs\n\
-+ Print instantiations as SZS compliant proof.\n\
-";
-
-InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option,
-                                                      const std::string& flag,
-                                                      const std::string& optarg)
-{
-  if(optarg == "default") {
-    return InstFormatMode::DEFAULT;
-  } else if(optarg == "szs") {
-    return InstFormatMode::SZS;
-  } else if(optarg == "help") {
-    puts(s_instFormatHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --inst-format: `") +
-                          optarg + "'.  Try --inst-format help.");
-  }
-}
-
 void OptionsHandler::setProduceAssertions(const std::string& option,
                                           const std::string& flag,
                                           bool value)
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index f19e63445..d6b81525d 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -183,10 +183,6 @@ public:
 
   /** Pointer to the containing Options object.*/
   Options* d_options;
-
-  /* Help strings */
-  static const std::string s_instFormatHelp;
-
 }; /* class OptionHandler */
 
 }  // namespace options
diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml
index 433e6f613..a8b11c197 100644
--- a/src/options/printer_options.toml
+++ b/src/options/printer_options.toml
@@ -17,25 +17,6 @@ name   = "Printing"
   help = "Print functional expressions over finite domains in a table format."
 
 [[option]]
-  name       = "instFormatMode"
-  category   = "regular"
-  long       = "inst-format=MODE"
-  type       = "InstFormatMode"
-  default    = "InstFormatMode::DEFAULT"
-  handler    = "stringToInstFormatMode"
-  includes   = ["options/printer_modes.h"]
-  help       = "print format mode for instantiations, see --inst-format=help"
-# InstFormatMode is currently exported as public so we can't auto genenerate
-# the enum.
-#  help_mode  = "Inst format modes."
-#[[option.mode.DEFAULT]]
-#  name = "default"
-#  help = "Print instantiations as a list in the output language format."
-#[[option.mode.SZS]]
-#  name = "szs"
-#  help = "Print instantiations as SZS compliant proof."
-
-[[option]]
   name       = "flattenHOChains"
   category   = "regular"
   long       = "flatten-ho-chains"
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index f0458793e..071f14dec 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -18,6 +18,9 @@ name   = "Proof"
 [[option.mode.VERIT]]
   name       = "verit"
   help       = "Output veriT proof"
+[[option.mode.TPTP]]
+  name       = "tptp"
+  help       = "Output TPTP proof (work in progress)"
 
 [[option]]
   name       = "proofPrintConclusion"
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 58632aafc..1bd29684a 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 = "strict"
+  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/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index dc48bc2a6..c60e636bd 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -411,7 +411,7 @@ void PseudoBooleanProcessor::applyReplacements(
 
 void PseudoBooleanProcessor::clear()
 {
-  d_off.clear();
+  d_off.reset();
   d_pos.clear();
   d_neg.clear();
 }
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h
index 74ee67fa4..b5bb05138 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.h
+++ b/src/preprocessing/passes/pseudo_boolean_processor.h
@@ -21,6 +21,7 @@
 #ifndef CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
 #define CVC5__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
 
+#include <optional>
 #include <unordered_set>
 #include <vector>
 
@@ -29,7 +30,6 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "theory/substitutions.h"
-#include "util/maybe.h"
 #include "util/rational.h"
 
 namespace cvc5 {
@@ -100,7 +100,7 @@ class PseudoBooleanProcessor : public PreprocessingPass
   context::CDO<unsigned> d_pbs;
 
   // decompose into \sum pos >= neg + off
-  Maybe<Rational> d_off;
+  std::optional<Rational> d_off;
   std::vector<Node> d_pos;
   std::vector<Node> d_neg;
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 0308715e6..dd22416db 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -65,16 +65,13 @@ public:
   }
 };
 
-PropEngine::PropEngine(TheoryEngine* te,
-                       Env& env,
-                       ProofNodeManager* pnm)
+PropEngine::PropEngine(TheoryEngine* te, Env& env)
     : d_inCheckSat(false),
       d_theoryEngine(te),
       d_env(env),
       d_skdm(new SkolemDefManager(d_env.getContext(), d_env.getUserContext())),
       d_theoryProxy(nullptr),
       d_satSolver(nullptr),
-      d_pnm(pnm),
       d_cnfStream(nullptr),
       d_pfCnfStream(nullptr),
       d_ppm(nullptr),
@@ -84,6 +81,7 @@ PropEngine::PropEngine(TheoryEngine* te,
   Debug("prop") << "Constructing the PropEngine" << std::endl;
   context::Context* satContext = d_env.getContext();
   context::UserContext* userContext = d_env.getUserContext();
+  ProofNodeManager* pnm = d_env.getProofNodeManager();
   ResourceManager* rm = d_env.getResourceManager();
 
   options::DecisionMode dmode = options::decisionMode();
@@ -107,13 +105,8 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   // CNF stream and theory proxy required pointers to each other, make the
   // theory proxy first
-  d_theoryProxy = new TheoryProxy(this,
-                                  d_theoryEngine,
-                                  d_decisionEngine.get(),
-                                  d_skdm.get(),
-                                  satContext,
-                                  userContext,
-                                  pnm);
+  d_theoryProxy = new TheoryProxy(
+      this, d_theoryEngine, d_decisionEngine.get(), d_skdm.get(), d_env);
   d_cnfStream = new CnfStream(d_satSolver,
                               d_theoryProxy,
                               userContext,
@@ -124,17 +117,15 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   // connect theory proxy
   d_theoryProxy->finishInit(d_cnfStream);
+  bool satProofs = d_env.isSatProofProducing();
   // connect SAT solver
-  d_satSolver->initialize(
-      d_env.getContext(),
-      d_theoryProxy,
-      d_env.getUserContext(),
-      options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS
-          ? pnm
-          : nullptr);
+  d_satSolver->initialize(d_env.getContext(),
+                          d_theoryProxy,
+                          d_env.getUserContext(),
+                          satProofs ? pnm : nullptr);
 
   d_decisionEngine->finishInit(d_satSolver, d_cnfStream);
-  if (pnm && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS)
+  if (satProofs)
   {
     d_pfCnfStream.reset(new ProofCnfStream(
         userContext,
@@ -670,7 +661,7 @@ bool PropEngine::properExplanation(TNode node, TNode expl) const
 
 void PropEngine::checkProof(context::CDList<Node>* assertions)
 {
-  if (!d_pnm)
+  if (!d_env.isSatProofProducing())
   {
     return;
   }
@@ -681,7 +672,7 @@ ProofCnfStream* PropEngine::getProofCnfStream() { return d_pfCnfStream.get(); }
 
 std::shared_ptr<ProofNode> PropEngine::getProof()
 {
-  if (!d_pnm)
+  if (!d_env.isSatProofProducing())
   {
     return nullptr;
   }
@@ -706,7 +697,7 @@ std::shared_ptr<ProofNode> PropEngine::getRefutation()
   Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS);
   std::vector<Node> core;
   getUnsatCore(core);
-  CDProof cdp(d_pnm);
+  CDProof cdp(d_env.getProofNodeManager());
   Node fnode = NodeManager::currentNM()->mkConst(false);
   cdp.addStep(fnode, PfRule::SAT_REFUTATION, core, {});
   return cdp.getProofFor(fnode);
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 4d06adfba..d26a425c8 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -56,9 +56,7 @@ class PropEngine
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(TheoryEngine* te,
-             Env& env,
-             ProofNodeManager* pnm);
+  PropEngine(TheoryEngine* te, Env& env);
 
   /**
    * Destructor.
@@ -372,9 +370,6 @@ class PropEngine
   /** List of all of the assertions that need to be made */
   std::vector<Node> d_assertionList;
 
-  /** A pointer to the proof node maneger to be used by this engine. */
-  ProofNodeManager* d_pnm;
-
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
   /** Proof-producing CNF converter */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 47263af97..c18fe2dd4 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -24,6 +24,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/skolem_def_manager.h"
+#include "smt/env.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
@@ -36,16 +37,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
                          TheoryEngine* theoryEngine,
                          decision::DecisionEngine* decisionEngine,
                          SkolemDefManager* skdm,
-                         context::Context* context,
-                         context::UserContext* userContext,
-                         ProofNodeManager* pnm)
+                         Env& env)
     : d_propEngine(propEngine),
       d_cnfStream(nullptr),
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
-      d_queue(context),
-      d_tpp(*theoryEngine, userContext, pnm),
-      d_skdm(skdm)
+      d_queue(env.getContext()),
+      d_tpp(*theoryEngine, env.getUserContext(), env.getProofNodeManager()),
+      d_skdm(skdm),
+      d_env(env)
 {
 }
 
@@ -98,8 +98,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
 
   TrustNode tte = d_theoryEngine->getExplanation(lNode);
   Node theoryExplanation = tte.getNode();
-  if (options::produceProofs()
-      && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS)
+  if (d_env.isSatProofProducing())
   {
     Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
            || tte.getGenerator());
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index f988c00e2..0e54ff8c9 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -35,10 +35,12 @@
 
 namespace cvc5 {
 
+class Env;
+class TheoryEngine;
+
 namespace decision {
 class DecisionEngine;
 }
-class TheoryEngine;
 
 namespace prop {
 
@@ -56,9 +58,7 @@ class TheoryProxy : public Registrar
               TheoryEngine* theoryEngine,
               decision::DecisionEngine* decisionEngine,
               SkolemDefManager* skdm,
-              context::Context* context,
-              context::UserContext* userContext,
-              ProofNodeManager* pnm);
+              Env& env);
 
   ~TheoryProxy();
 
@@ -162,6 +162,9 @@ class TheoryProxy : public Registrar
 
   /** The skolem definition manager */
   SkolemDefManager* d_skdm;
+
+  /** Reference to the environment */
+  Env& d_env;
 }; /* class TheoryProxy */
 
 }  // namespace prop
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index b7688d833..6292b5982 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -178,12 +178,19 @@ void Assertions::addFormula(TNode n,
     if (expr::hasFreeVar(n))
     {
       std::stringstream se;
-      se << "Cannot process assertion with free variable.";
-      if (language::isInputLangSygus(options::inputLanguage()))
+      if (isFunDef)
       {
-        // Common misuse of SyGuS is to use top-level assert instead of
-        // constraint when defining the synthesis conjecture.
-        se << " Perhaps you meant `constraint` instead of `assert`?";
+        se << "Cannot process function definition with free variable.";
+      }
+      else
+      {
+        se << "Cannot process assertion with free variable.";
+        if (language::isInputLangSygus(options::inputLanguage()))
+        {
+          // Common misuse of SyGuS is to use top-level assert instead of
+          // constraint when defining the synthesis conjecture.
+          se << " Perhaps you meant `constraint` instead of `assert`?";
+        }
       }
       throw ModalException(se.str().c_str());
     }
@@ -205,9 +212,11 @@ void Assertions::addDefineFunDefinition(Node n, bool global)
   }
   else
   {
-    // we don't check for free variables here, since even if we are sygus,
-    // we could contain functions-to-synthesize within definitions.
-    addFormula(n, true, false, true, false);
+    // We don't permit functions-to-synthesize within recursive function
+    // definitions currently. Thus, we should check for free variables if the
+    // input language is SyGuS.
+    bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
+    addFormula(n, true, false, true, maybeHasFv);
   }
 }
 
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index bb501fa5c..7aa05dde1 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2047,11 +2047,9 @@ GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
 bool GetInstantiationsCommand::isEnabled(api::Solver* solver,
                                          const api::Result& res)
 {
-  return (solver->getOptions().printer.instFormatMode
-              != options::InstFormatMode::SZS
-          && (res.isSat()
-              || (res.isSatUnknown()
-                  && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
+  return (res.isSat()
+          || (res.isSatUnknown()
+              && res.getUnknownExplanation() == api::Result::INCOMPLETE))
          || res.isUnsat() || res.isEntailed();
 }
 void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm)
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index a4e07d2c9..d6677c343 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -65,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);
@@ -81,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::isSatProofProducing() const
+{
+  return d_proofNodeManager != nullptr
+         && (!d_options.smt.unsatCores
+             || d_options.smt.unsatCoresMode
+                    != options::UnsatCoresMode::ASSUMPTIONS);
+}
+
 bool Env::isTheoryProofProducing() const
 {
   return d_proofNodeManager != nullptr
diff --git a/src/smt/env.h b/src/smt/env.h
index fa2fe6ab8..68148ec00 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -82,6 +82,16 @@ class Env
    */
   ProofNodeManager* getProofNodeManager();
 
+  /** Return the input name, or the empty string if not set */
+  const std::string& getFilename() const;
+
+  /**
+   * Check whether the SAT solver should produce proofs. Other than whether
+   * the proof node manager is set, SAT proofs are only generated when the
+   * unsat core mode is not ASSUMPTIONS.
+   */
+  bool isSatProofProducing() 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
@@ -133,6 +143,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 ------------------------------------------------------- */
   /**
@@ -199,6 +214,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/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp
new file mode 100644
index 000000000..ae35b346c
--- /dev/null
+++ b/src/smt/proof_final_callback.cpp
@@ -0,0 +1,109 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Haniel Barbosa, 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.
+ * ****************************************************************************
+ *
+ * Implementation of module for final processing proof nodes.
+ */
+
+#include "smt/proof_final_callback.h"
+
+#include "options/proof_options.h"
+#include "proof/proof_checker.h"
+#include "proof/proof_node_manager.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/builtin/proof_checker.h"
+#include "theory/theory_id.h"
+
+using namespace cvc5::kind;
+using namespace cvc5::theory;
+
+namespace cvc5 {
+namespace smt {
+
+ProofFinalCallback::ProofFinalCallback(ProofNodeManager* pnm)
+    : d_ruleCount(smtStatisticsRegistry().registerHistogram<PfRule>(
+          "finalProof::ruleCount")),
+      d_instRuleIds(
+          smtStatisticsRegistry().registerHistogram<theory::InferenceId>(
+              "finalProof::instRuleId")),
+      d_totalRuleCount(
+          smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")),
+      d_minPedanticLevel(
+          smtStatisticsRegistry().registerInt("finalProof::minPedanticLevel")),
+      d_numFinalProofs(
+          smtStatisticsRegistry().registerInt("finalProofs::numFinalProofs")),
+      d_pnm(pnm),
+      d_pedanticFailure(false)
+{
+  d_minPedanticLevel += 10;
+}
+
+void ProofFinalCallback::initializeUpdate()
+{
+  d_pedanticFailure = false;
+  d_pedanticFailureOut.str("");
+  ++d_numFinalProofs;
+}
+
+bool ProofFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
+                                      const std::vector<Node>& fa,
+                                      bool& continueUpdate)
+{
+  PfRule r = pn->getRule();
+  // if not doing eager pedantic checking, fail if below threshold
+  if (!options::proofEagerChecking())
+  {
+    if (!d_pedanticFailure)
+    {
+      Assert(d_pedanticFailureOut.str().empty());
+      if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
+      {
+        d_pedanticFailure = true;
+      }
+    }
+  }
+  uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
+  if (plevel != 0)
+  {
+    d_minPedanticLevel.minAssign(plevel);
+  }
+  // record stats for the rule
+  d_ruleCount << r;
+  ++d_totalRuleCount;
+  // take stats on the instantiations in the proof
+  if (r == PfRule::INSTANTIATE)
+  {
+    Node q = pn->getChildren()[0]->getResult();
+    const std::vector<Node>& args = pn->getArguments();
+    if (args.size() > q[0].getNumChildren())
+    {
+      InferenceId id;
+      if (getInferenceId(args[q[0].getNumChildren()], id))
+      {
+        d_instRuleIds << id;
+      }
+    }
+  }
+  return false;
+}
+
+bool ProofFinalCallback::wasPedanticFailure(std::ostream& out) const
+{
+  if (d_pedanticFailure)
+  {
+    out << d_pedanticFailureOut.str();
+    return true;
+  }
+  return false;
+}
+
+}  // namespace smt
+}  // namespace cvc5
diff --git a/src/smt/proof_final_callback.h b/src/smt/proof_final_callback.h
new file mode 100644
index 000000000..88b8e20ef
--- /dev/null
+++ b/src/smt/proof_final_callback.h
@@ -0,0 +1,74 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Haniel Barbosa, 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.
+ * ****************************************************************************
+ *
+ * The module for final processing proof nodes.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__SMT__PROOF_FINAL_CALLBACK_H
+#define CVC5__SMT__PROOF_FINAL_CALLBACK_H
+
+#include <map>
+#include <sstream>
+#include <unordered_set>
+
+#include "proof/proof_node_updater.h"
+#include "theory/inference_id.h"
+#include "util/statistics_stats.h"
+
+namespace cvc5 {
+namespace smt {
+
+/** Final callback class, for stats and pedantic checking */
+class ProofFinalCallback : public ProofNodeUpdaterCallback
+{
+ public:
+  ProofFinalCallback(ProofNodeManager* pnm);
+  /**
+   * Initialize, called once for each new ProofNode to process. This initializes
+   * static information to be used by successive calls to update.
+   */
+  void initializeUpdate();
+  /** Should proof pn be updated? Returns false, adds to stats. */
+  bool shouldUpdate(std::shared_ptr<ProofNode> pn,
+                    const std::vector<Node>& fa,
+                    bool& continueUpdate) override;
+  /** was pedantic failure */
+  bool wasPedanticFailure(std::ostream& out) const;
+
+ private:
+  /** Counts number of postprocessed proof nodes for each kind of proof rule */
+  HistogramStat<PfRule> d_ruleCount;
+  /**
+   * Counts number of postprocessed proof nodes of rule INSTANTIATE that were
+   * marked with the given inference id.
+   */
+  HistogramStat<theory::InferenceId> d_instRuleIds;
+  /** Total number of postprocessed rule applications */
+  IntStat d_totalRuleCount;
+  /** The minimum pedantic level of any rule encountered */
+  IntStat d_minPedanticLevel;
+  /** The total number of final proofs */
+  IntStat d_numFinalProofs;
+  /** Proof node manager (used for pedantic checking) */
+  ProofNodeManager* d_pnm;
+  /** Was there a pedantic failure? */
+  bool d_pedanticFailure;
+  /** The pedantic failure string for debugging */
+  std::stringstream d_pedanticFailureOut;
+};
+
+}  // namespace smt
+}  // namespace cvc5
+
+#endif
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 2c04b9e76..718d6cd6d 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -23,17 +23,19 @@
 #include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
 #include "smt/assertions.h"
+#include "smt/env.h"
 #include "smt/preprocess_proof_generator.h"
 #include "smt/proof_post_processor.h"
 
 namespace cvc5 {
 namespace smt {
 
-PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
-    : d_pchecker(new ProofChecker(options::proofPedantic())),
+PfManager::PfManager(Env& env, SmtEngine* smte)
+    : d_env(env),
+      d_pchecker(new ProofChecker(options::proofPedantic())),
       d_pnm(new ProofNodeManager(d_pchecker.get())),
       d_pppg(new PreprocessProofGenerator(
-          d_pnm.get(), u, "smt::PreprocessProofGenerator")),
+          d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),
       d_pfpp(new ProofPostproccess(
           d_pnm.get(),
           smte,
@@ -157,6 +159,13 @@ void PfManager::printProof(std::ostream& out,
     proof::DotPrinter dotPrinter;
     dotPrinter.print(out, fp.get());
   }
+  else if (options::proofFormatMode() == options::ProofFormatMode::TPTP)
+  {
+    out << "% SZS output start Proof for " << d_env.getFilename() << std::endl;
+    // TODO (proj #37) print in TPTP compliant format
+    out << *fp;
+    out << "% SZS output end Proof for " << d_env.getFilename() << std::endl;
+  }
   else
   {
     out << "(proof\n";
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 57478573c..fd24f62f6 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -23,6 +23,7 @@
 
 namespace cvc5 {
 
+class Env;
 class ProofChecker;
 class ProofNode;
 class ProofNodeManager;
@@ -70,7 +71,7 @@ class ProofPostproccess;
 class PfManager
 {
  public:
-  PfManager(context::UserContext* u, SmtEngine* smte);
+  PfManager(Env& env, SmtEngine* smte);
   ~PfManager();
   /**
    * Print the proof on the given output stream.
@@ -116,6 +117,8 @@ class PfManager
    */
   void getAssertions(Assertions& as,
                      std::vector<Node>& assertions);
+  /** Reference to the env of SmtEngine */
+  Env& d_env;
   /** The false node */
   Node d_false;
   /** For the new proofs module */
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 66f9fde7c..98ec30093 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -21,7 +21,6 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "proof/proof_node_manager.h"
 #include "smt/smt_engine.h"
-#include "smt/smt_statistics_registry.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/rewriter.h"
@@ -1179,84 +1178,6 @@ bool ProofPostprocessCallback::addToTransChildren(Node eq,
   return true;
 }
 
-ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
-    ProofNodeManager* pnm)
-    : d_ruleCount(smtStatisticsRegistry().registerHistogram<PfRule>(
-          "finalProof::ruleCount")),
-      d_instRuleIds(
-          smtStatisticsRegistry().registerHistogram<theory::InferenceId>(
-              "finalProof::instRuleId")),
-      d_totalRuleCount(
-          smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")),
-      d_minPedanticLevel(
-          smtStatisticsRegistry().registerInt("finalProof::minPedanticLevel")),
-      d_numFinalProofs(
-          smtStatisticsRegistry().registerInt("finalProofs::numFinalProofs")),
-      d_pnm(pnm),
-      d_pedanticFailure(false)
-{
-  d_minPedanticLevel += 10;
-}
-
-void ProofPostprocessFinalCallback::initializeUpdate()
-{
-  d_pedanticFailure = false;
-  d_pedanticFailureOut.str("");
-  ++d_numFinalProofs;
-}
-
-bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
-                                                 const std::vector<Node>& fa,
-                                                 bool& continueUpdate)
-{
-  PfRule r = pn->getRule();
-  // if not doing eager pedantic checking, fail if below threshold
-  if (!options::proofEagerChecking())
-  {
-    if (!d_pedanticFailure)
-    {
-      Assert(d_pedanticFailureOut.str().empty());
-      if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut))
-      {
-        d_pedanticFailure = true;
-      }
-    }
-  }
-  uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r);
-  if (plevel != 0)
-  {
-    d_minPedanticLevel.minAssign(plevel);
-  }
-  // record stats for the rule
-  d_ruleCount << r;
-  ++d_totalRuleCount;
-  // take stats on the instantiations in the proof
-  if (r == PfRule::INSTANTIATE)
-  {
-    Node q = pn->getChildren()[0]->getResult();
-    const std::vector<Node>& args = pn->getArguments();
-    if (args.size() > q[0].getNumChildren())
-    {
-      InferenceId id;
-      if (getInferenceId(args[q[0].getNumChildren()], id))
-      {
-        d_instRuleIds << id;
-      }
-    }
-  }
-  return false;
-}
-
-bool ProofPostprocessFinalCallback::wasPedanticFailure(std::ostream& out) const
-{
-  if (d_pedanticFailure)
-  {
-    out << d_pedanticFailureOut.str();
-    return true;
-  }
-  return false;
-}
-
 ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
                                      SmtEngine* smte,
                                      ProofGenerator* pppg,
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index 056f77695..1aa52dd50 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -23,6 +23,7 @@
 #include <unordered_set>
 
 #include "proof/proof_node_updater.h"
+#include "smt/proof_final_callback.h"
 #include "smt/witness_form.h"
 #include "theory/inference_id.h"
 #include "util/statistics_stats.h"
@@ -237,45 +238,6 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
                              CDProof* cdp);
 };
 
-/** Final callback class, for stats and pedantic checking */
-class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
-{
- public:
-  ProofPostprocessFinalCallback(ProofNodeManager* pnm);
-  /**
-   * Initialize, called once for each new ProofNode to process. This initializes
-   * static information to be used by successive calls to update.
-   */
-  void initializeUpdate();
-  /** Should proof pn be updated? Returns false, adds to stats. */
-  bool shouldUpdate(std::shared_ptr<ProofNode> pn,
-                    const std::vector<Node>& fa,
-                    bool& continueUpdate) override;
-  /** was pedantic failure */
-  bool wasPedanticFailure(std::ostream& out) const;
-
- private:
-  /** Counts number of postprocessed proof nodes for each kind of proof rule */
-  HistogramStat<PfRule> d_ruleCount;
-  /**
-   * Counts number of postprocessed proof nodes of rule INSTANTIATE that were
-   * marked with the given inference id.
-   */
-  HistogramStat<theory::InferenceId> d_instRuleIds;
-  /** Total number of postprocessed rule applications */
-  IntStat d_totalRuleCount;
-  /** The minimum pedantic level of any rule encountered */
-  IntStat d_minPedanticLevel;
-  /** The total number of final proofs */
-  IntStat d_numFinalProofs;
-  /** Proof node manager (used for pedantic checking) */
-  ProofNodeManager* d_pnm;
-  /** Was there a pedantic failure? */
-  bool d_pedanticFailure;
-  /** The pedantic failure string for debugging */
-  std::stringstream d_pedanticFailureOut;
-};
-
 /**
  * The proof postprocessor module. This postprocesses the final proof
  * produced by an SmtEngine. Its main two tasks are to:
@@ -314,7 +276,7 @@ class ProofPostproccess
    */
   ProofNodeUpdater d_updater;
   /** The post process callback for finalization */
-  ProofPostprocessFinalCallback d_finalCb;
+  ProofFinalCallback d_finalCb;
   /**
    * The finalizer, which is responsible for taking stats and checking for
    * (lazy) pedantic failures.
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 6fd2a3f68..12433d8ac 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1104,13 +1104,6 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts)
     }
   }
   // implied options...
-  if (opts.quantifiers.strictTriggers)
-  {
-    if (!opts.quantifiers.userPatternsQuantWasSetByUser)
-    {
-      opts.quantifiers.userPatternsQuant = options::UserPatMode::TRUST;
-    }
-  }
   if (opts.quantifiers.qcfModeWasSetByUser || opts.quantifiers.qcfTConstraint)
   {
     opts.quantifiers.quantConflictFind = true;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 3e4c1efa7..0ddac7202 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -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)),
@@ -203,7 +203,7 @@ void SmtEngine::finishInit()
     // ensure bound variable uses canonical bound variables
     getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
     // make the proof manager
-    d_pfManager.reset(new PfManager(getUserContext(), this));
+    d_pfManager.reset(new PfManager(*d_env.get(), this));
     PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
     // start the unsat core manager
     d_ucManager.reset(new UnsatCoreManager());
@@ -213,8 +213,6 @@ void SmtEngine::finishInit()
     d_env->setProofNodeManager(pnm);
     // enable it in the assertions pipeline
     d_asserts->setProofGenerator(pppg);
-    // enable it in the SmtSolver
-    d_smtSolver->setProofNodeManager(pnm);
     // enabled proofs in the preprocessor
     d_pp->setProofGenerator(pppg);
   }
@@ -381,7 +379,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.
@@ -391,7 +389,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) {
@@ -436,7 +434,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)
   {
@@ -728,7 +726,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);
 }
@@ -944,7 +942,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());
   }
 }
 
@@ -1213,7 +1211,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;
 }
@@ -1601,11 +1599,6 @@ std::string SmtEngine::getProof()
 void SmtEngine::printInstantiations( std::ostream& out ) {
   SmtScope smts(this);
   finishInit();
-  if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
-  {
-    out << "% SZS output start Proof for " << d_state->getFilename()
-        << std::endl;
-  }
   QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations");
 
   // First, extract and print the skolemizations
@@ -1692,10 +1685,6 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   {
     out << "none" << std::endl;
   }
-  if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
-  {
-    out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
-  }
 }
 
 void SmtEngine::getInstantiationTermVectors(
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 595a3808c..214193b00 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -40,7 +40,6 @@ SmtSolver::SmtSolver(Env& env,
       d_state(state),
       d_pp(pp),
       d_stats(stats),
-      d_pnm(nullptr),
       d_theoryEngine(nullptr),
       d_propEngine(nullptr)
 {
@@ -61,16 +60,17 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
     theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id);
   }
   // Add the proof checkers for each theory
-  if (d_pnm)
+  ProofNodeManager* pnm = d_env.getProofNodeManager();
+  if (pnm)
   {
-    d_theoryEngine->initializeProofChecker(d_pnm->getChecker());
+    d_theoryEngine->initializeProofChecker(pnm->getChecker());
   }
   Trace("smt-debug") << "Making prop engine..." << std::endl;
   /* force destruction of referenced PropEngine to enforce that statistics
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env, d_pnm));
+  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -86,7 +86,7 @@ void SmtSolver::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env, d_pnm));
+  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env));
   d_theoryEngine->setPropEngine(getPropEngine());
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not
@@ -133,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())
   {
@@ -236,8 +236,6 @@ void SmtSolver::processAssertions(Assertions& as)
   as.clearCurrent();
 }
 
-void SmtSolver::setProofNodeManager(ProofNodeManager* pnm) { d_pnm = pnm; }
-
 TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
 
 prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }
diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index cf82d9309..cdc98606c 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -114,11 +114,6 @@ class SmtSolver
    * into the SMT solver, and clears the buffer.
    */
   void processAssertions(Assertions& as);
-  /**
-   * Set proof node manager. Enables proofs in this SmtSolver. Should be
-   * called before finishInit.
-   */
-  void setProofNodeManager(ProofNodeManager* pnm);
   //------------------------------------------ access methods
   /** Get a pointer to the TheoryEngine owned by this solver. */
   TheoryEngine* getTheoryEngine();
@@ -139,11 +134,6 @@ class SmtSolver
   Preprocessor& d_pp;
   /** Reference to the statistics of SmtEngine */
   SmtEngineStatistics& d_stats;
-  /**
-   * Pointer to the proof node manager used by this SmtSolver. A non-null
-   * proof node manager indicates that proofs are enabled.
-   */
-  ProofNodeManager* d_pnm;
   /** The theory engine */
   std::unique_ptr<TheoryEngine> d_theoryEngine;
   /** The propositional engine */
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 33860d2d9..89d7619cf 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -308,16 +308,17 @@ Rational ApproximateSimplex::estimateWithCFE(const Rational& r, const Integer& K
   }
 }
 
-Maybe<Rational> ApproximateSimplex::estimateWithCFE(double d, const Integer& D)
+std::optional<Rational> ApproximateSimplex::estimateWithCFE(double d,
+                                                            const Integer& D)
 {
-  if (Maybe<Rational> from_double = Rational::fromDouble(d))
+  if (std::optional<Rational> from_double = Rational::fromDouble(d))
   {
-    return estimateWithCFE(from_double.value(), D);
+    return estimateWithCFE(*from_double, D);
   }
-  return Maybe<Rational>();
+  return std::optional<Rational>();
 }
 
-Maybe<Rational> ApproximateSimplex::estimateWithCFE(double d)
+std::optional<Rational> ApproximateSimplex::estimateWithCFE(double d)
 {
   return estimateWithCFE(d, s_defaultMaxDenom);
 }
@@ -1106,9 +1107,9 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
         }
 
         DeltaRational proposal;
-        if (Maybe<Rational> maybe_new = estimateWithCFE(newAssign))
+        if (std::optional maybe_new = estimateWithCFE(newAssign))
         {
-          proposal = maybe_new.value();
+          proposal = *maybe_new;
         }
         else
         {
@@ -2055,13 +2056,13 @@ bool ApproxGLPK::attemptBranchCut(int nid, const BranchCutInfo& br_cut){
   d_pad.d_cut.lhs.set(x, Rational(1));
 
   Rational& rhs = d_pad.d_cut.rhs;
-  Maybe<Rational> br_cut_rhs = Rational::fromDouble(br_cut.getRhs());
+  std::optional<Rational> br_cut_rhs = Rational::fromDouble(br_cut.getRhs());
   if (!br_cut_rhs)
   {
     return true;
   }
 
-  rhs = estimateWithCFE(br_cut_rhs.value(), Integer(1));
+  rhs = estimateWithCFE(*br_cut_rhs, Integer(1));
   d_pad.d_failure = !rhs.isIntegral();
   if(d_pad.d_failure) { return true; }
 
@@ -2112,13 +2113,13 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){
   DenseMap<Rational>& alpha = d_pad.d_alpha.lhs;
   Rational& b = d_pad.d_alpha.rhs;
 
-  Maybe<Rational> delta = estimateWithCFE(mir.delta);
+  std::optional<Rational> delta = estimateWithCFE(mir.delta);
   if (!delta)
   {
     return true;
   }
 
-  d_pad.d_failure = (delta.value().sgn() <= 0);
+  d_pad.d_failure = (delta->sgn() <= 0);
   if(d_pad.d_failure){ return true; }
 
   Debug("approx::mir") << "applyCMIRRule() " << delta << " " << mir.delta << endl;
@@ -2128,7 +2129,7 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){
   for(; iter != iend; ++iter){
     ArithVar v = *iter;
     const Rational& curr = alpha[v];
-    Rational next = curr / delta.value();
+    Rational next = curr / *delta;
     if(compRanges.isKey(v)){
       b -= curr * compRanges[v];
       alpha.set(v, - next);
@@ -2136,7 +2137,7 @@ bool ApproxGLPK::applyCMIRRule(int nid, const MirInfo& mir){
       alpha.set(v, next);
     }
   }
-  b = b / delta.value();
+  b = b / *delta;
 
   Rational roundB = (b + Rational(1,2)).floor();
   d_pad.d_failure = (b - roundB).abs() < Rational(1,90);
@@ -2554,7 +2555,7 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){
     double coeff = row_sum.coeffs[i];
     ArithVar x = _getArithVar(nid, M, aux_ind);
     if(x == ARITHVAR_SENTINEL){ return true; }
-    Maybe<Rational> c = estimateWithCFE(coeff);
+    std::optional<Rational> c = estimateWithCFE(coeff);
     if (!c)
     {
       return true;
@@ -2562,11 +2563,11 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){
 
     if (lhs.isKey(x))
     {
-      lhs.get(x) -= c.value();
+      lhs.get(x) -= *c;
     }
     else
     {
-      lhs.set(x, -c.value());
+      lhs.set(x, -(*c));
     }
   }
 
@@ -2586,13 +2587,13 @@ bool ApproxGLPK::loadRowSumIntoAgg(int nid, int M, const PrimitiveVec& row_sum){
     double coeff = row_sum.coeffs[i];
     ArithVar x = _getArithVar(nid, M, aux_ind);
     Assert(x != ARITHVAR_SENTINEL);
-    Maybe<Rational> c = estimateWithCFE(coeff);
+    std::optional<Rational> c = estimateWithCFE(coeff);
     if (!c)
     {
       return true;
     }
     Assert(!lhs.isKey(x));
-    lhs.set(x, c.value());
+    lhs.set(x, *c);
   }
 
   if(Debug.isOn("approx::mir")){
@@ -3023,12 +3024,12 @@ bool ApproxGLPK::guessCoefficientsConstructTableRow(int nid, int M, const Primit
     }
     Debug("guessCoefficientsConstructTableRow") << "match " << ind << "," << var << "("<<d_vars.asNode(var)<<")"<<endl;
 
-    Maybe<Rational> cfe = estimateWithCFE(coeff, D);
+    std::optional<Rational> cfe = estimateWithCFE(coeff, D);
     if (!cfe)
     {
       return true;
     }
-    tab.set(var, cfe.value());
+    tab.set(var, *cfe);
     Debug("guessCoefficientsConstructTableRow") << var << " cfe " << cfe << endl;
   }
   if(!guessIsConstructable(tab)){
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index aeced6f10..c0d6990a4 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -19,12 +19,13 @@
 #include "cvc5_private.h"
 
 #pragma once
+
+#include <optional>
 #include <vector>
 
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
 #include "util/dense_map.h"
-#include "util/maybe.h"
 #include "util/rational.h"
 #include "util/statistics_stats.h"
 
@@ -126,8 +127,8 @@ class ApproximateSimplex{
    * cuts off the estimate once the value is approximately zero.
    * This is designed for removing rounding artifacts.
    */
-  static Maybe<Rational> estimateWithCFE(double d);
-  static Maybe<Rational> estimateWithCFE(double d, const Integer& D);
+  static std::optional<Rational> estimateWithCFE(double d);
+  static std::optional<Rational> estimateWithCFE(double d, const Integer& D);
 
   /**
    * Converts a rational to a continued fraction expansion representation
diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp
index 07f24f0f0..4cbb8211d 100644
--- a/src/theory/arith/infer_bounds.cpp
+++ b/src/theory/arith/infer_bounds.cpp
@@ -35,20 +35,21 @@ InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a)
   Assert(a != Simplex);
 }
 
-InferBoundAlgorithm::InferBoundAlgorithm(const Maybe<int>& simplexRounds)
-  : d_alg(Simplex)
+InferBoundAlgorithm::InferBoundAlgorithm(
+    const std::optional<int>& simplexRounds)
+    : d_alg(Simplex)
 {}
 
 Algorithms InferBoundAlgorithm::getAlgorithm() const{
   return d_alg;
 }
 
-const Maybe<int>& InferBoundAlgorithm::getSimplexRounds() const{
+const std::optional<int>& InferBoundAlgorithm::getSimplexRounds() const
+{
   Assert(getAlgorithm() == Simplex);
   return d_simplexRounds;
 }
 
-
 InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){
   return InferBoundAlgorithm(Lookup);
 }
@@ -57,7 +58,9 @@ InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){
   return InferBoundAlgorithm(RowSum);
 }
 
-InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){
+InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(
+    const std::optional<int>& rounds)
+{
   return InferBoundAlgorithm(rounds);
 }
 
diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
index 8a65c7c66..22b0b5d54 100644
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.h
@@ -20,12 +20,12 @@
 
 #pragma once
 
+#include <optional>
 #include <ostream>
 
 #include "expr/node.h"
 #include "theory/arith/delta_rational.h"
 #include "util/integer.h"
-#include "util/maybe.h"
 #include "util/rational.h"
 
 namespace cvc5 {
@@ -39,19 +39,19 @@ namespace inferbounds {
 class InferBoundAlgorithm {
 private:
   Algorithms d_alg;
-  Maybe<int> d_simplexRounds;
+  std::optional<int> d_simplexRounds;
   InferBoundAlgorithm(Algorithms a);
-  InferBoundAlgorithm(const Maybe<int>& simplexRounds);
+  InferBoundAlgorithm(const std::optional<int>& simplexRounds);
 
-public:
+ public:
   InferBoundAlgorithm();
 
   Algorithms getAlgorithm() const;
-  const Maybe<int>& getSimplexRounds() const;
+  const std::optional<int>& getSimplexRounds() const;
 
   static InferBoundAlgorithm mkLookup();
   static InferBoundAlgorithm mkRowSum();
-  static InferBoundAlgorithm mkSimplex(const Maybe<int>& rounds);
+  static InferBoundAlgorithm mkSimplex(const std::optional<int>& rounds);
 };
 
 std::ostream& operator<<(std::ostream& os, const Algorithms a);
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 82cc02815..47dd208c1 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -1054,14 +1054,12 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr
   Assert(nbSgn != 0);
 
   if(nbSgn > 0){
-    if (d_upperBoundDifference.nothing()
-        || nbDiff <= d_upperBoundDifference.value())
+    if (!d_upperBoundDifference || nbDiff <= *d_upperBoundDifference)
     {
       return false;
     }
   }else{
-    if (d_lowerBoundDifference.nothing()
-        || nbDiff >= d_lowerBoundDifference.value())
+    if (!d_lowerBoundDifference || nbDiff >= *d_lowerBoundDifference)
     {
       return false;
     }
@@ -1132,8 +1130,8 @@ UpdateInfo LinearEqualityModule::mkConflictUpdate(const Tableau::Entry& entry, b
 UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational& focusCoeff, UpdatePreferenceFunction pref){
   Assert(d_increasing.empty());
   Assert(d_decreasing.empty());
-  Assert(d_lowerBoundDifference.nothing());
-  Assert(d_upperBoundDifference.nothing());
+  Assert(!d_lowerBoundDifference);
+  Assert(!d_upperBoundDifference);
 
   int focusCoeffSgn = focusCoeff.sgn();
 
@@ -1146,14 +1144,14 @@ UpdateInfo LinearEqualityModule::speculativeUpdate(ArithVar nb, const Rational&
   if(d_variables.hasUpperBound(nb)){
     ConstraintP ub = d_variables.getUpperBoundConstraint(nb);
     d_upperBoundDifference = ub->getValue() - d_variables.getAssignment(nb);
-    Border border(ub, d_upperBoundDifference.value(), false, NULL, true);
+    Border border(ub, *d_upperBoundDifference, false, NULL, true);
     Debug("handleBorders") << "push back increasing " << border << endl;
     d_increasing.push_back(border);
   }
   if(d_variables.hasLowerBound(nb)){
     ConstraintP lb = d_variables.getLowerBoundConstraint(nb);
     d_lowerBoundDifference = lb->getValue() - d_variables.getAssignment(nb);
-    Border border(lb, d_lowerBoundDifference.value(), false, NULL, false);
+    Border border(lb, *d_lowerBoundDifference, false, NULL, false);
     Debug("handleBorders") << "push back decreasing " << border << endl;
     d_decreasing.push_back(border);
   }
@@ -1189,8 +1187,8 @@ void LinearEqualityModule::clearSpeculative(){
   // clear everything away
   d_increasing.clear();
   d_decreasing.clear();
-  d_lowerBoundDifference.clear();
-  d_upperBoundDifference.clear();
+  d_lowerBoundDifference.reset();
+  d_upperBoundDifference.reset();
 }
 
 void LinearEqualityModule::handleBorders(UpdateInfo& selected, ArithVar nb, const Rational& focusCoeff, BorderHeap& heap, int minimumFixes, UpdatePreferenceFunction pref){
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 276c8e63e..7195a6583 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -37,7 +37,6 @@
 #include "theory/arith/partial_model.h"
 #include "theory/arith/simplex_update.h"
 #include "theory/arith/tableau.h"
-#include "util/maybe.h"
 #include "util/statistics_stats.h"
 
 namespace cvc5 {
@@ -216,8 +215,8 @@ private:
 
   BorderHeap d_increasing;
   BorderHeap d_decreasing;
-  Maybe<DeltaRational> d_upperBoundDifference;
-  Maybe<DeltaRational> d_lowerBoundDifference;
+  std::optional<DeltaRational> d_upperBoundDifference;
+  std::optional<DeltaRational> d_lowerBoundDifference;
 
   Rational d_one;
   Rational d_negOne;
diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index 7db6c266f..b196f9990 100644
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -30,20 +30,18 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-ExtState::ExtState(InferenceManager& im,
-                   NlModel& model,
-                   ProofNodeManager* pnm,
-                   context::UserContext* c)
-    : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c)
+ExtState::ExtState(InferenceManager& im, NlModel& model, Env& env)
+    : d_im(im), d_model(model), d_env(env)
 {
   d_false = NodeManager::currentNM()->mkConst(false);
   d_true = NodeManager::currentNM()->mkConst(true);
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
-  if (d_pnm != nullptr)
+  if (d_env.isTheoryProofProducing())
   {
-    d_proof.reset(new CDProofSet<CDProof>(d_pnm, d_ctx, "nl-ext"));
+    d_proof.reset(new CDProofSet<CDProof>(
+        d_env.getProofNodeManager(), d_env.getUserContext(), "nl-ext"));
   }
 }
 
@@ -105,7 +103,7 @@ bool ExtState::isProofEnabled() const { return d_proof.get() != nullptr; }
 CDProof* ExtState::getProof()
 {
   Assert(isProofEnabled());
-  return d_proof->allocateProof(d_ctx);
+  return d_proof->allocateProof(d_env.getUserContext());
 }
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index 7c2cc1b9b..ac00f6f87 100644
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -20,6 +20,7 @@
 
 #include "expr/node.h"
 #include "proof/proof_set.h"
+#include "smt/env.h"
 #include "theory/arith/nl/ext/monomial.h"
 
 namespace cvc5 {
@@ -37,10 +38,7 @@ class NlModel;
 
 struct ExtState
 {
-  ExtState(InferenceManager& im,
-           NlModel& model,
-           ProofNodeManager* pnm,
-           context::UserContext* c);
+  ExtState(InferenceManager& im, NlModel& model, Env& env);
 
   void init(const std::vector<Node>& xts);
 
@@ -63,13 +61,8 @@ struct ExtState
   InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
-  /**
-   * Pointer to the current proof node manager. nullptr, if proofs are
-   * disabled.
-   */
-  ProofNodeManager* d_pnm;
-  /** The user context. */
-  context::UserContext* d_ctx;
+  /** Reference to the environment */
+  Env& d_env;
   /**
    * A CDProofSet that hands out CDProof objects for lemmas.
    */
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 0deb2c99d..31bc4c662 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -207,7 +207,7 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
       }
       // compute if bound is not satisfied, and store what is required
       // for a possible refinement
-      if (options::nlExtTangentPlanes())
+      if (d_data->d_env.getOptions().arith.nlExtTangentPlanes)
       {
         if (is_false_lit)
         {
diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index 6d9faa356..dcd6398b5 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -29,7 +29,7 @@ namespace arith {
 namespace nl {
 
 SplitZeroCheck::SplitZeroCheck(ExtState* data)
-    : d_data(data), d_zero_split(d_data->d_ctx)
+    : d_data(data), d_zero_split(d_data->d_env.getUserContext())
 {
 }
 
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 785127db5..df531fca7 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -37,27 +37,29 @@ namespace arith {
 namespace nl {
 
 NonlinearExtension::NonlinearExtension(TheoryArith& containing,
-                                       ArithState& state,
-                                       eq::EqualityEngine* ee,
-                                       ProofNodeManager* pnm)
+                                       ArithState& state)
     : d_containing(containing),
+      d_astate(state),
       d_im(containing.getInferenceManager()),
       d_needsLastCall(false),
       d_checkCounter(0),
-      d_extTheoryCb(ee),
+      d_extTheoryCb(state.getEqualityEngine()),
       d_extTheory(d_extTheoryCb,
                   containing.getSatContext(),
                   containing.getUserContext(),
                   d_im),
       d_model(containing.getSatContext()),
-      d_trSlv(d_im, d_model, pnm, containing.getUserContext()),
-      d_extState(d_im, d_model, pnm, containing.getUserContext()),
+      d_trSlv(d_im, d_model, d_astate.getEnv()),
+      d_extState(d_im, d_model, d_astate.getEnv()),
       d_factoringSlv(&d_extState),
       d_monomialBoundsSlv(&d_extState),
       d_monomialSlv(&d_extState),
       d_splitZeroSlv(&d_extState),
       d_tangentPlaneSlv(&d_extState),
-      d_cadSlv(d_im, d_model, state.getUserContext(), pnm),
+      d_cadSlv(d_im,
+               d_model,
+               state.getUserContext(),
+               d_astate.getEnv().getProofNodeManager()),
       d_icpSlv(d_im),
       d_iandSlv(d_im, state, d_model),
       d_pow2Slv(d_im, state, d_model)
@@ -73,9 +75,9 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
 
-  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
-  if (pc != nullptr)
+  if (d_astate.getEnv().isTheoryProofProducing())
   {
+    ProofChecker* pc = d_astate.getEnv().getProofNodeManager()->getChecker();
     d_proofChecker.registerTo(pc);
   }
 }
@@ -94,6 +96,11 @@ void NonlinearExtension::processSideEffect(const NlLemma& se)
   d_trSlv.processSideEffect(se);
 }
 
+const Options& NonlinearExtension::options() const
+{
+  return d_containing.options();
+}
+
 void NonlinearExtension::computeRelevantAssertions(
     const std::vector<Node>& assertions, std::vector<Node>& keep)
 {
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index aae19df6e..6cbbfcdac 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -84,10 +84,7 @@ class NonlinearExtension
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  NonlinearExtension(TheoryArith& containing,
-                     ArithState& state,
-                     eq::EqualityEngine* ee,
-                     ProofNodeManager* pnm);
+  NonlinearExtension(TheoryArith& containing, ArithState& state);
   ~NonlinearExtension();
   /**
    * Does non-context dependent setup for a node connected to a theory.
@@ -145,6 +142,9 @@ class NonlinearExtension
   /** Process side effect se */
   void processSideEffect(const NlLemma& se);
 
+  /** Obtain options object */
+  const Options& options() const;
+
  private:
   /** Model-based refinement
    *
@@ -223,6 +223,8 @@ class NonlinearExtension
   Node d_true;
   // The theory of arithmetic containing this extension.
   TheoryArith& d_containing;
+  /** A reference to the arithmetic state object */
+  ArithState& d_astate;
   InferenceManager& d_im;
   /** The statistics class */
   NlStats d_stats;
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index e5fa31aad..2b1ef0a2e 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -603,39 +603,39 @@ Node excluding_interval_to_lemma(const Node& variable,
   return nm->mkNode(Kind::OR, lb, ub);
 }
 
-Maybe<Rational> get_lower_bound(const Node& n)
+std::optional<Rational> get_lower_bound(const Node& n)
 {
-  if (n.getNumChildren() != 2) return Maybe<Rational>();
+  if (n.getNumChildren() != 2) return std::optional<Rational>();
   if (n.getKind() == Kind::LT)
   {
-    if (!n[0].isConst()) return Maybe<Rational>();
-    if (!n[1].isVar()) return Maybe<Rational>();
+    if (!n[0].isConst()) return std::optional<Rational>();
+    if (!n[1].isVar()) return std::optional<Rational>();
     return n[0].getConst<Rational>();
   }
   else if (n.getKind() == Kind::GT)
   {
-    if (!n[0].isVar()) return Maybe<Rational>();
-    if (!n[1].isConst()) return Maybe<Rational>();
+    if (!n[0].isVar()) return std::optional<Rational>();
+    if (!n[1].isConst()) return std::optional<Rational>();
     return n[1].getConst<Rational>();
   }
-  return Maybe<Rational>();
+  return std::optional<Rational>();
 }
-Maybe<Rational> get_upper_bound(const Node& n)
+std::optional<Rational> get_upper_bound(const Node& n)
 {
-  if (n.getNumChildren() != 2) return Maybe<Rational>();
+  if (n.getNumChildren() != 2) return std::optional<Rational>();
   if (n.getKind() == Kind::LT)
   {
-    if (!n[0].isVar()) return Maybe<Rational>();
-    if (!n[1].isConst()) return Maybe<Rational>();
+    if (!n[0].isVar()) return std::optional<Rational>();
+    if (!n[1].isConst()) return std::optional<Rational>();
     return n[1].getConst<Rational>();
   }
   else if (n.getKind() == Kind::GT)
   {
-    if (!n[0].isConst()) return Maybe<Rational>();
-    if (!n[1].isVar()) return Maybe<Rational>();
+    if (!n[0].isConst()) return std::optional<Rational>();
+    if (!n[1].isVar()) return std::optional<Rational>();
     return n[0].getConst<Rational>();
   }
-  return Maybe<Rational>();
+  return std::optional<Rational>();
 }
 
 /** Returns indices of appropriate parts of ran encoding.
@@ -675,12 +675,12 @@ std::tuple<Node, Rational, Rational> detect_ran_encoding(const Node& n)
     Assert(false) << "Invalid polynomial equation.";
   }
 
-  Maybe<Rational> lower = get_lower_bound(n[0]);
+  std::optional<Rational> lower = get_lower_bound(n[0]);
   if (!lower) lower = get_lower_bound(n[1]);
   if (!lower) lower = get_lower_bound(n[2]);
   Assert(lower) << "Could not identify lower bound.";
 
-  Maybe<Rational> upper = get_upper_bound(n[0]);
+  std::optional<Rational> upper = get_upper_bound(n[0]);
   if (!upper) upper = get_upper_bound(n[1]);
   if (!upper) upper = get_upper_bound(n[2]);
   Assert(upper) << "Could not identify upper bound.";
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 0d5e5ad04..c7bb14b3f 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -39,11 +39,10 @@ namespace transcendental {
 
 TranscendentalSolver::TranscendentalSolver(InferenceManager& im,
                                            NlModel& m,
-                                           ProofNodeManager* pnm,
-                                           context::UserContext* c)
-    : d_tstate(im, m, pnm, c), d_expSlv(&d_tstate), d_sineSlv(&d_tstate)
+                                           Env& env)
+    : d_tstate(im, m, env), d_expSlv(&d_tstate), d_sineSlv(&d_tstate)
 {
-  d_taylor_degree = options::nlExtTfTaylorDegree();
+  d_taylor_degree = d_tstate.d_env.getOptions().arith.nlExtTfTaylorDegree;
 }
 
 TranscendentalSolver::~TranscendentalSolver() {}
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h
index 54bad2c1d..b63ebf29d 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.h
@@ -50,10 +50,7 @@ namespace transcendental {
 class TranscendentalSolver
 {
  public:
-  TranscendentalSolver(InferenceManager& im,
-                       NlModel& m,
-                       ProofNodeManager* pnm,
-                       context::UserContext* c);
+  TranscendentalSolver(InferenceManager& im, NlModel& m, Env& env);
   ~TranscendentalSolver();
 
   /** init last call
@@ -187,7 +184,7 @@ class TranscendentalSolver
    * initially to options::nlExtTfTaylorDegree() and may be incremented
    * if the option options::nlExtTfIncPrecision() is enabled.
    */
-  unsigned d_taylor_degree;
+  uint64_t d_taylor_degree;
 
   /** Common state for transcendental solver */
   transcendental::TranscendentalState d_tstate;
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index db20713f1..19a334729 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -30,20 +30,20 @@ namespace transcendental {
 
 TranscendentalState::TranscendentalState(InferenceManager& im,
                                          NlModel& model,
-                                         ProofNodeManager* pnm,
-                                         context::UserContext* c)
-    : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c)
+                                         Env& env)
+    : d_im(im), d_model(model), d_env(env)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_one = NodeManager::currentNM()->mkConst(Rational(1));
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
-  if (d_pnm != nullptr)
+  if (d_env.isTheoryProofProducing())
   {
-    d_proof.reset(new CDProofSet<CDProof>(d_pnm, d_ctx, "nl-trans"));
+    d_proof.reset(new CDProofSet<CDProof>(
+        d_env.getProofNodeManager(), d_env.getUserContext(), "nl-trans"));
     d_proofChecker.reset(new TranscendentalProofRuleChecker());
-    d_proofChecker->registerTo(pnm->getChecker());
+    d_proofChecker->registerTo(d_env.getProofNodeManager()->getChecker());
   }
 }
 
@@ -55,7 +55,7 @@ bool TranscendentalState::isProofEnabled() const
 CDProof* TranscendentalState::getProof()
 {
   Assert(isProofEnabled());
-  return d_proof->allocateProof(d_ctx);
+  return d_proof->allocateProof(d_env.getUserContext());
 }
 
 void TranscendentalState::init(const std::vector<Node>& xts,
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 56cbec79a..65215c83c 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -18,6 +18,7 @@
 
 #include "expr/node.h"
 #include "proof/proof_set.h"
+#include "smt/env.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/transcendental/proof_checker.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
@@ -61,10 +62,7 @@ inline std::ostream& operator<<(std::ostream& os, Convexity c) {
  */
 struct TranscendentalState
 {
-  TranscendentalState(InferenceManager& im,
-                      NlModel& model,
-                      ProofNodeManager* pnm,
-                      context::UserContext* c);
+  TranscendentalState(InferenceManager& im, NlModel& model, Env& env);
 
   /**
    * Checks whether proofs are enabled.
@@ -170,16 +168,11 @@ struct TranscendentalState
   InferenceManager& d_im;
   /** Reference to the non-linear model object */
   NlModel& d_model;
+  /** Reference to the environment */
+  Env& d_env;
   /** Utility to compute taylor approximations */
   TaylorGenerator d_taylor;
   /**
-   * Pointer to the current proof node manager. nullptr, if proofs are
-   * disabled.
-   */
-  ProofNodeManager* d_pnm;
-  /** The user context. */
-  context::UserContext* d_ctx;
-  /**
    * A CDProofSet that hands out CDProof objects for lemmas.
    */
   std::unique_ptr<CDProofSet<CDProof>> d_proof;
diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp
index dc01a9b42..78e58000e 100644
--- a/src/theory/arith/simplex_update.cpp
+++ b/src/theory/arith/simplex_update.cpp
@@ -14,6 +14,7 @@
  */
 
 #include "theory/arith/simplex_update.h"
+
 #include "theory/arith/constraint.h"
 
 using namespace std;
@@ -22,6 +23,22 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
+/*
+ * Generates a string representation of std::optional and inserts it into a
+ * stream.
+ *
+ * Note: We define this function here in the cvc5::theory::arith namespace,
+ * because it would otherwise not be found for std::optional<int>. This is due
+ * to the argument-dependent lookup rules.
+ *
+ * @param out The stream
+ * @param m The value
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, const std::optional<int>& m)
+{
+  return cvc5::operator<<(out, m);
+}
 
 UpdateInfo::UpdateInfo():
   d_nonbasic(ARITHVAR_SENTINEL),
@@ -72,7 +89,7 @@ void UpdateInfo::updateUnbounded(const DeltaRational& delta, int ec, int f){
   d_nonbasicDelta = delta;
   d_errorsChange = ec;
   d_focusDirection = f;
-  d_tableauCoefficient.clear();
+  d_tableauCoefficient.reset();
   updateWitness();
   Assert(unbounded());
   Assert(improvement(d_witness));
@@ -82,9 +99,9 @@ void UpdateInfo::updateUnbounded(const DeltaRational& delta, int ec, int f){
 void UpdateInfo::updatePureFocus(const DeltaRational& delta, ConstraintP c){
   d_limiting = c;
   d_nonbasicDelta = delta;
-  d_errorsChange.clear();
+  d_errorsChange.reset();
   d_focusDirection = 1;
-  d_tableauCoefficient.clear();
+  d_tableauCoefficient.reset();
   updateWitness();
   Assert(!describesPivot());
   Assert(improvement(d_witness));
@@ -94,8 +111,8 @@ void UpdateInfo::updatePureFocus(const DeltaRational& delta, ConstraintP c){
 void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c){
   d_limiting = c;
   d_nonbasicDelta = delta;
-  d_errorsChange.clear();
-  d_focusDirection.clear();
+  d_errorsChange.reset();
+  d_focusDirection.reset();
   updateWitness();
   Assert(describesPivot());
   Assert(debugSgnAgreement());
@@ -105,7 +122,7 @@ void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, Cons
   d_limiting = c;
   d_nonbasicDelta = delta;
   d_errorsChange = ec;
-  d_focusDirection.clear();
+  d_focusDirection.reset();
   d_tableauCoefficient = &r;
   updateWitness();
   Assert(describesPivot());
@@ -117,7 +134,7 @@ void UpdateInfo::witnessedUpdate(const DeltaRational& delta, ConstraintP c, int
   d_nonbasicDelta = delta;
   d_errorsChange = ec;
   d_focusDirection = fd;
-  d_tableauCoefficient.clear();
+  d_tableauCoefficient.reset();
   updateWitness();
   Assert(describesPivot() || improvement(d_witness));
   Assert(debugSgnAgreement());
diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h
index 6216f53f6..7efa51acb 100644
--- a/src/theory/arith/simplex_update.h
+++ b/src/theory/arith/simplex_update.h
@@ -29,10 +29,11 @@
 
 #pragma once
 
-#include "theory/arith/delta_rational.h"
+#include <optional>
+
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
-#include "util/maybe.h"
+#include "theory/arith/delta_rational.h"
 
 namespace cvc5 {
 namespace theory {
@@ -109,7 +110,7 @@ private:
    * This is changed via the updateProposal(...) methods.
    * The value needs to satisfy debugSgnAgreement() or it is in conflict.
    */
-  Maybe<DeltaRational> d_nonbasicDelta;
+  std::optional<DeltaRational> d_nonbasicDelta;
 
   /**
    * This is true if the pivot-and-update is *known* to cause a conflict.
@@ -118,16 +119,16 @@ private:
   bool d_foundConflict;
 
   /** This is the change in the size of the error set. */
-  Maybe<int> d_errorsChange;
+  std::optional<int> d_errorsChange;
 
   /** This is the sgn of the change in the value of the focus set.*/
-  Maybe<int> d_focusDirection;
+  std::optional<int> d_focusDirection;
 
   /** This is the sgn of the change in the value of the focus set.*/
-  Maybe<DeltaRational> d_focusChange;
+  std::optional<DeltaRational> d_focusChange;
 
   /** This is the coefficient in the tableau for the entry.*/
-  Maybe<const Rational*> d_tableauCoefficient;
+  std::optional<const Rational*> d_tableauCoefficient;
 
   /**
    * This is the constraint that nonbasic is basic is updating s.t. its variable is against it.
@@ -329,18 +330,19 @@ private:
     if(d_foundConflict){
       return ConflictFound;
     }
-    else if (d_errorsChange.just() && d_errorsChange.value() < 0)
+    else if (d_errorsChange && d_errorsChange.value() < 0)
     {
       return ErrorDropped;
     }
-    else if (d_errorsChange.nothing() || d_errorsChange.value() == 0)
+    else if (d_errorsChange.value_or(0) == 0)
     {
-      if(d_focusDirection.just()){
-        if (d_focusDirection.value() > 0)
+      if (d_focusDirection)
+      {
+        if (*d_focusDirection > 0)
         {
           return FocusImproved;
         }
-        else if (d_focusDirection.value() == 0)
+        else if (*d_focusDirection == 0)
         {
           return Degenerate;
         }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 37069d8b8..aabf017a8 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -44,8 +44,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
       d_ppre(getSatContext(), d_pnm),
       d_bab(d_astate, d_im, d_ppre, d_pnm),
       d_eqSolver(nullptr),
-      d_internal(new TheoryArithPrivate(
-          *this, getSatContext(), getUserContext(), d_bab, d_pnm)),
+      d_internal(new TheoryArithPrivate(*this, env, d_bab)),
       d_nonlinearExtension(nullptr),
       d_opElim(d_pnm, getLogicInfo()),
       d_arithPreproc(d_astate, d_im, d_pnm, d_opElim),
@@ -102,8 +101,7 @@ void TheoryArith::finishInit()
   const LogicInfo& logicInfo = getLogicInfo();
   if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
   {
-    d_nonlinearExtension.reset(
-        new nl::NonlinearExtension(*this, d_astate, d_equalityEngine, d_pnm));
+    d_nonlinearExtension.reset(new nl::NonlinearExtension(*this, d_astate));
   }
   if (d_eqSolver != nullptr)
   {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c85376e6b..ea2887c44 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/theory_arith_private.h"
 
 #include <map>
+#include <optional>
 #include <queue>
 #include <vector>
 
@@ -85,19 +86,19 @@ static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum)
 static bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap);
 
 TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
-                                       context::Context* c,
-                                       context::UserContext* u,
-                                       BranchAndBound& bab,
-                                       ProofNodeManager* pnm)
+                                       Env& env,
+                                       BranchAndBound& bab)
     : d_containing(containing),
+      d_env(env),
       d_foundNl(false),
       d_rowTracking(),
       d_bab(bab),
-      d_pnm(pnm),
+      d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager()
+                                           : nullptr),
       d_checker(),
-      d_pfGen(new EagerProofGenerator(d_pnm, u)),
-      d_constraintDatabase(c,
-                           u,
+      d_pfGen(new EagerProofGenerator(d_pnm, d_env.getUserContext())),
+      d_constraintDatabase(d_env.getContext(),
+                           d_env.getUserContext(),
                            d_partialModel,
                            d_congruenceManager,
                            RaiseConflict(*this),
@@ -106,15 +107,15 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_qflraStatus(Result::SAT_UNKNOWN),
       d_unknownsInARow(0),
       d_hasDoneWorkSinceCut(false),
-      d_learner(u),
-      d_assertionsThatDoNotMatchTheirLiterals(c),
+      d_learner(d_env.getUserContext()),
+      d_assertionsThatDoNotMatchTheirLiterals(d_env.getContext()),
       d_nextIntegerCheckVar(0),
-      d_constantIntegerVariables(c),
-      d_diseqQueue(c, false),
+      d_constantIntegerVariables(d_env.getContext()),
+      d_diseqQueue(d_env.getContext(), false),
       d_currentPropagationList(),
-      d_learnedBounds(c),
-      d_preregisteredNodes(u),
-      d_partialModel(c, DeltaComputeCallback(*this)),
+      d_learnedBounds(d_env.getContext()),
+      d_preregisteredNodes(d_env.getUserContext()),
+      d_partialModel(d_env.getContext(), DeltaComputeCallback(*this)),
       d_errorSet(
           d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(*this)),
       d_tableau(),
@@ -122,22 +123,23 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
               d_tableau,
               d_rowTracking,
               BasicVarModelUpdateCallBack(*this)),
-      d_diosolver(c),
+      d_diosolver(d_env.getContext()),
       d_restartsCounter(0),
       d_tableauSizeHasBeenModified(false),
       d_tableauResetDensity(1.6),
       d_tableauResetPeriod(10),
-      d_conflicts(c),
-      d_blackBoxConflict(c, Node::null()),
-      d_blackBoxConflictPf(c, std::shared_ptr<ProofNode>(nullptr)),
-      d_congruenceManager(c,
-                          u,
+      d_conflicts(d_env.getContext()),
+      d_blackBoxConflict(d_env.getContext(), Node::null()),
+      d_blackBoxConflictPf(d_env.getContext(),
+                           std::shared_ptr<ProofNode>(nullptr)),
+      d_congruenceManager(d_env.getContext(),
+                          d_env.getUserContext(),
                           d_constraintDatabase,
                           SetupLiteralCallBack(*this),
                           d_partialModel,
                           RaiseEqualityEngineConflict(*this),
                           d_pnm),
-      d_cmEnabled(c, options::arithCongMan()),
+      d_cmEnabled(d_env.getContext(), options().arith.arithCongMan),
 
       d_dualSimplex(
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
@@ -149,22 +151,22 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
           d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)),
       d_pass1SDP(NULL),
       d_otherSDP(NULL),
-      d_lastContextIntegerAttempted(c, -1),
+      d_lastContextIntegerAttempted(d_env.getContext(), -1),
 
       d_DELTA_ZERO(0),
-      d_approxCuts(c),
+      d_approxCuts(d_env.getContext()),
       d_fullCheckCounter(0),
-      d_cutCount(c, 0),
-      d_cutInContext(c),
-      d_likelyIntegerInfeasible(c, false),
-      d_guessedCoeffSet(c, false),
+      d_cutCount(d_env.getContext(), 0),
+      d_cutInContext(d_env.getContext()),
+      d_likelyIntegerInfeasible(d_env.getContext(), false),
+      d_guessedCoeffSet(d_env.getContext(), false),
       d_guessedCoeffs(),
       d_treeLog(NULL),
       d_replayVariables(),
       d_replayConstraints(),
       d_lhsTmp(),
       d_approxStats(NULL),
-      d_attemptSolveIntTurnedOff(u, 0),
+      d_attemptSolveIntTurnedOff(d_env.getUserContext(), 0),
       d_dioSolveResources(0),
       d_solveIntMaybeHelp(0u),
       d_solveIntAttempts(0u),
@@ -508,13 +510,13 @@ bool TheoryArithPrivate::getDioCuttingResource(){
   if(d_dioSolveResources > 0){
     d_dioSolveResources--;
     if(d_dioSolveResources == 0){
-      d_dioSolveResources = -options::rrTurns();
+      d_dioSolveResources = -options().arith.rrTurns;
     }
     return true;
   }else{
     d_dioSolveResources++;
     if(d_dioSolveResources >= 0){
-      d_dioSolveResources = options::dioSolverTurns();
+      d_dioSolveResources = options().arith.dioSolverTurns;
     }
     return false;
   }
@@ -1046,7 +1048,7 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(
       // Add the substitution if not recursive
       Assert(elim == Rewriter::rewrite(elim));
 
-      if (right.size() > options::ppAssertMaxSubSize())
+      if (right.size() > options().arith.ppAssertMaxSubSize)
       {
         Debug("simplify")
             << "TheoryArithPrivate::solve(): did not substitute due to the "
@@ -1881,7 +1883,10 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em
 
   if(d_qflraStatus == Result::UNSAT){ return false; }
   if(emmmittedLemmaOrSplit){ return false; }
-  if(!options::useApprox()){ return false; }
+  if (!options().arith.useApprox)
+  {
+    return false;
+  }
   if(!ApproximateSimplex::enabled()){ return false; }
 
   if(Theory::fullEffort(effortLevel)){
@@ -1901,8 +1906,10 @@ bool TheoryArithPrivate::attemptSolveInteger(Theory::Effort effortLevel, bool em
     }
   }
 
-
-  if(!options::trySolveIntStandardEffort()){ return false; }
+  if (!options().arith.trySolveIntStandardEffort)
+  {
+    return false;
+  }
 
   if (d_lastContextIntegerAttempted <= (level >> 2))
   {
@@ -2066,7 +2073,8 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(
     if(d_partialModel.hasNode(v)){
       d_lhsTmp.set(v, Rational(1));
       double dval = nl.branchValue();
-      Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval);
+      std::optional<Rational> maybe_value =
+          ApproximateSimplex::estimateWithCFE(dval);
       if (!maybe_value)
       {
         return make_pair(NullConstraint, ARITHVAR_SENTINEL);
@@ -2350,7 +2358,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
 
         if(ci->reconstructed() && ci->proven()){
           const DenseMap<Rational>& row = ci->getReconstruction().lhs;
-          reject = !complexityBelow(row, options::replayRejectCutSize());
+          reject = !complexityBelow(row, options().arith.replayRejectCutSize);
         }
       }
       if(conflictQueueEmpty()){
@@ -2398,8 +2406,9 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
 
     /* check if the system is feasible under with the cuts */
     if(conflictQueueEmpty()){
-      Assert(options::replayEarlyCloseDepths() >= 1);
-      if(!nl.isBranch() || depth % options::replayEarlyCloseDepths() == 0 ){
+      Assert(options().arith.replayEarlyCloseDepths >= 1);
+      if (!nl.isBranch() || depth % options().arith.replayEarlyCloseDepths == 0)
+      {
         TimerStat::CodeTimer codeTimer(d_statistics.d_replaySimplexTimer);
         //test for linear feasibility
         d_partialModel.stopQueueingBoundCounts();
@@ -2513,8 +2522,8 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
     resolveOutPropagated(res, propagated);
     Debug("approx::replayLogRec") << "replayLogRec() ending" << std::endl;
 
-
-    if(options::replayFailureLemma()){
+    if (options().arith.replayFailureLemma)
+    {
       // must be done inside the sat context to get things
       // propagated at this level
       if(res.empty() && nid == getTreeLog().getRootId()){
@@ -2609,7 +2618,8 @@ Node TheoryArithPrivate::branchToNode(ApproximateSimplex* approx,
     if(d_partialModel.hasNode(v)){
       Node n = d_partialModel.asNode(v);
       double dval = bn.branchValue();
-      Maybe<Rational> maybe_value = ApproximateSimplex::estimateWithCFE(dval);
+      std::optional<Rational> maybe_value =
+          ApproximateSimplex::estimateWithCFE(dval);
       if (!maybe_value)
       {
         return Node::null();
@@ -2656,7 +2666,8 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
       Assert(cut->proven());
 
       const DenseMap<Rational>& row =  cut->getReconstruction().lhs;
-      if(!complexityBelow(row, options::lemmaRejectCutSize())){
+      if (!complexityBelow(row, options().arith.lemmaRejectCutSize))
+      {
         ++(d_statistics.d_cutsRejectedDuringLemmas);
         continue;
       }
@@ -2743,7 +2754,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
   }
 
   // if integers are attempted,
-  Assert(options::useApprox());
+  Assert(options().arith.useApprox);
   Assert(ApproximateSimplex::enabled());
 
   int level = getSatContext()->getLevel();
@@ -2766,8 +2777,9 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
       approx->setOptCoeffs(d_guessedCoeffs);
     }
     static const int32_t depthForLikelyInfeasible = 10;
-    int maxDepthPass1 = d_likelyIntegerInfeasible ?
-      depthForLikelyInfeasible : options::maxApproxDepth();
+    int maxDepthPass1 = d_likelyIntegerInfeasible
+                            ? depthForLikelyInfeasible
+                            : options().arith.maxApproxDepth;
     approx->setBranchingDepth(maxDepthPass1);
     approx->setBranchOnVariableLimit(100);
     LinResult relaxRes = approx->solveRelaxation();
@@ -2830,7 +2842,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
           }
         }
         if(!(anyConflict() || !d_approxCuts.empty())){
-          turnOffApproxFor(options::replayNumericFailurePenalty());
+          turnOffApproxFor(options().arith.replayNumericFailurePenalty);
         }
         break;
       case BranchesExhausted:
@@ -2870,11 +2882,16 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){
 SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){
   if(pass1){
     if(d_pass1SDP == NULL){
-      if(options::useFC()){
+      if (options().arith.useFC)
+      {
         d_pass1SDP = (SimplexDecisionProcedure*)(&d_fcSimplex);
-      }else if(options::useSOI()){
+      }
+      else if (options().arith.useSOI)
+      {
         d_pass1SDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
-      }else{
+      }
+      else
+      {
         d_pass1SDP = (SimplexDecisionProcedure*)(&d_dualSimplex);
       }
     }
@@ -2882,13 +2899,18 @@ SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){
     return *d_pass1SDP;
   }else{
      if(d_otherSDP == NULL){
-      if(options::useFC()){
-        d_otherSDP  = (SimplexDecisionProcedure*)(&d_fcSimplex);
-      }else if(options::useSOI()){
-        d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
-      }else{
-        d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
-      }
+       if (options().arith.useFC)
+       {
+         d_otherSDP = (SimplexDecisionProcedure*)(&d_fcSimplex);
+       }
+       else if (options().arith.useSOI)
+       {
+         d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
+       }
+       else
+       {
+         d_otherSDP = (SimplexDecisionProcedure*)(&d_soiSimplex);
+       }
     }
     Assert(d_otherSDP != NULL);
     return *d_otherSDP;
@@ -2909,8 +2931,8 @@ void TheoryArithPrivate::importSolution(const ApproximateSimplex::Solution& solu
   }
 
   if(d_qflraStatus != Result::UNSAT){
-    static const int32_t pass2Limit = 20;
-    int16_t oldCap = options::arithStandardCheckVarOrderPivots();
+    static const int64_t pass2Limit = 20;
+    int64_t oldCap = options().arith.arithStandardCheckVarOrderPivots;
     Options::current().arith.arithStandardCheckVarOrderPivots = pass2Limit;
     SimplexDecisionProcedure& simplex = selectSimplex(false);
     d_qflraStatus = simplex.findModel(false);
@@ -2961,20 +2983,19 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
   d_partialModel.processBoundsQueue(utcb);
   d_linEq.startTrackingBoundCounts();
 
-  bool noPivotLimit = Theory::fullEffort(effortLevel) ||
-    !options::restrictedPivots();
+  bool noPivotLimit =
+      Theory::fullEffort(effortLevel) || !options().arith.restrictedPivots;
 
   SimplexDecisionProcedure& simplex = selectSimplex(true);
 
-  bool useApprox = options::useApprox() && ApproximateSimplex::enabled() && getSolveIntegerResource();
+  bool useApprox = options().arith.useApprox && ApproximateSimplex::enabled()
+                   && getSolveIntegerResource();
 
   Debug("TheoryArithPrivate::solveRealRelaxation")
-    << "solveRealRelaxation() approx"
-    << " " <<  options::useApprox()
-    << " " << ApproximateSimplex::enabled()
-    << " " << useApprox
-    << " " << safeToCallApprox()
-    << endl;
+      << "solveRealRelaxation() approx"
+      << " " << options().arith.useApprox << " "
+      << ApproximateSimplex::enabled() << " " << useApprox << " "
+      << safeToCallApprox() << endl;
 
   bool noPivotLimitPass1 = noPivotLimit && !useApprox;
   d_qflraStatus = simplex.findModel(noPivotLimitPass1);
@@ -3133,7 +3154,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
 
   if(anyConflict()){
     d_qflraStatus = Result::UNSAT;
-    if (options::revertArithModels() && d_previousStatus == Result::SAT)
+    if (options().arith.revertArithModels && d_previousStatus == Result::SAT)
     {
       ++d_statistics.d_revertsOnConflicts;
       Debug("arith::bt") << "clearing here "
@@ -3208,10 +3229,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
     if(Debug.isOn("arith::consistency")){
       Assert(entireStateIsConsistent("sat comit"));
     }
-    if(useSimplex && options::collectPivots()){
-      if(options::useFC()){
+    if (useSimplex && options().arith.collectPivots)
+    {
+      if (options().arith.useFC)
+      {
         d_statistics.d_satPivots << d_fcSimplex.getPivots();
-      }else{
+      }
+      else
+      {
         d_statistics.d_satPivots << d_dualSimplex.getPivots();
       }
     }
@@ -3226,10 +3251,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
     d_partialModel.commitAssignmentChanges();
     d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow);
 
-    if(useSimplex && options::collectPivots()){
-      if(options::useFC()){
+    if (useSimplex && options().arith.collectPivots)
+    {
+      if (options().arith.useFC)
+      {
         d_statistics.d_unknownPivots << d_fcSimplex.getPivots();
-      }else{
+      }
+      else
+      {
         d_statistics.d_unknownPivots << d_dualSimplex.getPivots();
       }
     }
@@ -3252,10 +3281,14 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
     emmittedConflictOrSplit = true;
     Debug("arith::conflict") << "simplex conflict" << endl;
 
-    if(useSimplex && options::collectPivots()){
-      if(options::useFC()){
+    if (useSimplex && options().arith.collectPivots)
+    {
+      if (options().arith.useFC)
+      {
         d_statistics.d_unsatPivots << d_fcSimplex.getPivots();
-      }else{
+      }
+      else
+      {
         d_statistics.d_unsatPivots << d_dualSimplex.getPivots();
       }
     }
@@ -3265,8 +3298,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
   }
   d_statistics.d_avgUnknownsInARow << d_unknownsInARow;
 
-  size_t nPivots =
-      options::useFC() ? d_fcSimplex.getPivots() : d_dualSimplex.getPivots();
+  size_t nPivots = options().arith.useFC ? d_fcSimplex.getPivots()
+                                         : d_dualSimplex.getPivots();
   for (std::size_t i = 0; i < nPivots; ++i)
   {
     d_containing.d_out->spendResource(
@@ -3295,9 +3328,9 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
 
   // This should be fine if sat or unknown
   if (!emmittedConflictOrSplit
-      && (options::arithPropagationMode()
+      && (options().arith.arithPropagationMode
               == options::ArithPropagationMode::UNATE_PROP
-          || options::arithPropagationMode()
+          || options().arith.arithPropagationMode
                  == options::ArithPropagationMode::BOTH_PROP))
   {
     TimerStat::CodeTimer codeTimer0(d_statistics.d_newPropTime);
@@ -3380,7 +3413,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
 
   if(!emmittedConflictOrSplit && Theory::fullEffort(effortLevel) && !hasIntegerModel()){
     Node possibleConflict = Node::null();
-    if(!emmittedConflictOrSplit && options::arithDioSolver()){
+    if (!emmittedConflictOrSplit && options().arith.arithDioSolver)
+    {
       possibleConflict = callDioSolver();
       if(possibleConflict != Node::null()){
         revertOutOfConflict();
@@ -3392,7 +3426,9 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
       }
     }
 
-    if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && options::arithDioSolver()){
+    if (!emmittedConflictOrSplit && d_hasDoneWorkSinceCut
+        && options().arith.arithDioSolver)
+    {
       if(getDioCuttingResource()){
         TrustNode possibleLemma = dioCutting();
         if(!possibleLemma.isNull()){
@@ -3422,7 +3458,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
       }
     }
 
-    if(options::maxCutsInContext() <= d_cutCount){
+    if (options().arith.maxCutsInContext <= d_cutCount)
+    {
       if(d_diosolver.hasMoreDecompositionLemmas()){
         while(d_diosolver.hasMoreDecompositionLemmas()){
           Node decompositionLemma = d_diosolver.nextDecompositionLemma();
@@ -3494,7 +3531,8 @@ std::vector<ArithVar> TheoryArithPrivate::cutAllBounded() const{
   vector<ArithVar> lemmas;
   ArithVar max = d_partialModel.getNumberOfVariables();
 
-  if(options::doCutAllBounded() && max > 0){
+  if (options().arith.doCutAllBounded && max > 0)
+  {
     for(ArithVar iter = 0; iter != max; ++iter){
     //Do not include slack variables
       const DeltaRational& d = d_partialModel.getAssignment(iter);
@@ -3642,15 +3680,18 @@ TrustNode TheoryArithPrivate::explain(TNode n)
 void TheoryArithPrivate::propagate(Theory::Effort e) {
   // This uses model values for safety. Disable for now.
   if (d_qflraStatus == Result::SAT
-      && (options::arithPropagationMode()
+      && (options().arith.arithPropagationMode
               == options::ArithPropagationMode::BOUND_INFERENCE_PROP
-          || options::arithPropagationMode()
+          || options().arith.arithPropagationMode
                  == options::ArithPropagationMode::BOTH_PROP)
       && hasAnyUpdates())
   {
-    if(options::newProp()){
+    if (options().arith.newProp)
+    {
       propagateCandidatesNew();
-    }else{
+    }
+    else
+    {
       propagateCandidates();
     }
   }
@@ -4019,8 +4060,10 @@ void TheoryArithPrivate::presolve(){
   }
 
   vector<TrustNode> lemmas;
-  if(!options::incrementalSolving()) {
-    switch(options::arithUnateLemmaMode()){
+  if (!options().base.incrementalSolving)
+  {
+    switch (options().arith.arithUnateLemmaMode)
+    {
       case options::ArithUnateLemmaMode::NO: break;
       case options::ArithUnateLemmaMode::INEQUALITY:
         d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
@@ -4032,7 +4075,7 @@ void TheoryArithPrivate::presolve(){
         d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
         d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
         break;
-      default: Unhandled() << options::arithUnateLemmaMode();
+      default: Unhandled() << options().arith.arithUnateLemmaMode;
     }
   }
 
@@ -4180,10 +4223,14 @@ void TheoryArithPrivate::propagateCandidates(){
   DenseSet::const_iterator end = d_updatedBounds.end();
   for(; i != end; ++i){
     ArithVar var = *i;
-    if(d_tableau.isBasic(var) &&
-       d_tableau.basicRowLength(var) <= options::arithPropagateMaxLength()){
+    if (d_tableau.isBasic(var)
+        && d_tableau.basicRowLength(var)
+               <= options().arith.arithPropagateMaxLength)
+    {
       d_candidateBasics.softAdd(var);
-    }else{
+    }
+    else
+    {
       Tableau::ColIterator basicIter = d_tableau.colIterator(var);
       for(; !basicIter.atEnd(); ++basicIter){
         const Tableau::Entry& entry = *basicIter;
@@ -4191,7 +4238,9 @@ void TheoryArithPrivate::propagateCandidates(){
         ArithVar rowVar = d_tableau.rowIndexToBasic(ridx);
         Assert(entry.getColVar() == var);
         Assert(d_tableau.isBasic(rowVar));
-        if(d_tableau.getRowLength(ridx) <= options::arithPropagateMaxLength()){
+        if (d_tableau.getRowLength(ridx)
+            <= options().arith.arithPropagateMaxLength)
+        {
           d_candidateBasics.softAdd(rowVar);
         }
       }
@@ -4425,7 +4474,8 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
     //   * coeffs[0] is for implied
     //   * coeffs[i+1] is for explain[i]
     d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs);
-    if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
+    if (d_tableau.getRowLength(ridx) <= options().arith.arithPropAsLemmaLength)
+    {
       if (Debug.isOn("arith::prop::pf")) {
         for (const auto & constraint : explain) {
           Assert(constraint->hasProof());
@@ -4490,7 +4540,9 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
       {
         outputLemma(clause, InferenceId::ARITH_ROW_IMPL);
       }
-    }else{
+    }
+    else
+    {
       Assert(!implied->negationHasProof());
       implied->impliedByFarkas(explain, coeffs, false);
       implied->tryToPropagate();
@@ -4518,9 +4570,9 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
   Debug("arith::prop")
     << "propagateCandidateRow " << instance << " attempt " << rowLength << " " <<  hasCount << endl;
 
-  if (rowLength >= options::arithPropagateMaxLength()
+  if (rowLength >= options().arith.arithPropagateMaxLength
       && Random::getRandom().pickWithProb(
-             1.0 - double(options::arithPropagateMaxLength()) / rowLength))
+          1.0 - double(options().arith.arithPropagateMaxLength) / rowLength))
   {
     return false;
   }
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 4afe121b9..0cdc031e1 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -88,6 +88,9 @@ private:
   static const uint32_t RESET_START = 2;
 
   TheoryArith& d_containing;
+  Env& d_env;
+
+  const Options& options() const { return d_env.getOptions(); }
 
   /**
    * Whether we encountered non-linear arithmetic at any time during solving.
@@ -423,11 +426,7 @@ private:
   DeltaRational getDeltaValue(TNode term) const
       /* throw(DeltaRationalException, ModelException) */;
  public:
-  TheoryArithPrivate(TheoryArith& containing,
-                     context::Context* c,
-                     context::UserContext* u,
-                     BranchAndBound& bab,
-                     ProofNodeManager* pnm);
+  TheoryArithPrivate(TheoryArith& containing, Env& env, BranchAndBound& bab);
   ~TheoryArithPrivate();
 
   //--------------------------------- initialization
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 0d56dd6db..9d25dd760 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -175,63 +175,5 @@ bool ModelManager::collectModelBooleanVariables()
   return true;
 }
 
-void ModelManager::collectAssertedTerms(TheoryId tid,
-                                        std::set<Node>& termSet,
-                                        bool includeShared) const
-{
-  Theory* t = d_te.theoryOf(tid);
-  // Collect all terms appearing in assertions
-  context::CDList<Assertion>::const_iterator assert_it = t->facts_begin(),
-                                             assert_it_end = t->facts_end();
-  for (; assert_it != assert_it_end; ++assert_it)
-  {
-    collectTerms(tid, *assert_it, termSet);
-  }
-
-  if (includeShared)
-  {
-    // Add terms that are shared terms
-    context::CDList<TNode>::const_iterator shared_it = t->shared_terms_begin(),
-                                           shared_it_end =
-                                               t->shared_terms_end();
-    for (; shared_it != shared_it_end; ++shared_it)
-    {
-      collectTerms(tid, *shared_it, termSet);
-    }
-  }
-}
-
-void ModelManager::collectTerms(TheoryId tid,
-                                TNode n,
-                                std::set<Node>& termSet) const
-{
-  const std::set<Kind>& irrKinds = d_model->getIrrelevantKinds();
-  std::vector<TNode> visit;
-  TNode cur;
-  visit.push_back(n);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    if (termSet.find(cur) != termSet.end())
-    {
-      // already visited
-      continue;
-    }
-    Kind k = cur.getKind();
-    // only add to term set if a relevant kind
-    if (irrKinds.find(k) == irrKinds.end())
-    {
-      termSet.insert(cur);
-    }
-    // traverse owned terms, don't go under quantifiers
-    if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == tid)
-        && !cur.isClosure())
-    {
-      visit.insert(visit.end(), cur.begin(), cur.end());
-    }
-  } while (!visit.empty());
-}
-
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index ff8459fcb..fd8ca6e11 100644
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -108,22 +108,7 @@ class ModelManager
    * @return true if we are in conflict.
    */
   bool collectModelBooleanVariables();
-  /**
-   * Collect asserted terms for theory with the given identifier, add to
-   * termSet.
-   *
-   * @param tid The theory whose assertions we are collecting
-   * @param termSet The set to add terms to
-   * @param includeShared Whether to include the shared terms of the theory
-   */
-  void collectAssertedTerms(TheoryId tid,
-                            std::set<Node>& termSet,
-                            bool includeShared = true) const;
-  /**
-   * Helper function for collectAssertedTerms, adds all subterms
-   * belonging to theory tid to termSet.
-   */
-  void collectTerms(TheoryId tid, TNode n, std::set<Node>& termSet) const;
+
   /** Reference to the theory engine */
   TheoryEngine& d_te;
   /** Reference to the environment */
diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp
index 4124407be..91e4cb6d4 100644
--- a/src/theory/model_manager_distributed.cpp
+++ b/src/theory/model_manager_distributed.cpp
@@ -81,11 +81,19 @@ bool ModelManagerDistributed::prepareModel()
       continue;
     }
     Theory* t = d_te.theoryOf(theoryId);
+    if (theoryId == TheoryId::THEORY_BOOL
+        || theoryId == TheoryId::THEORY_BUILTIN)
+    {
+      Trace("model-builder")
+          << "  Skipping theory " << theoryId
+          << " as it does not contribute to the model anyway" << std::endl;
+      continue;
+    }
     Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId
                            << std::endl;
     // collect the asserted terms
     std::set<Node> termSet;
-    collectAssertedTerms(theoryId, termSet);
+    t->collectAssertedTerms(termSet);
     // also get relevant terms
     t->computeRelevantTerms(termSet);
     if (!t->collectModelInfo(d_model.get(), termSet))
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..99949e223 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[2])
+    {
+      if (qc.getKind() == INST_PATTERN || qc.getKind() == INST_NO_PATTERN)
+      {
         hasPat = true;
         break;
       }
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/theory.cpp b/src/theory/theory.cpp
index b774d456a..5ca1979b3 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -387,6 +387,60 @@ void Theory::computeRelevantTerms(std::set<Node>& termSet)
   // by default, there are no additional relevant terms
 }
 
+void Theory::collectAssertedTerms(std::set<Node>& termSet,
+                                  bool includeShared) const
+{
+  // Collect all terms appearing in assertions
+  context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
+                                             assert_it_end = facts_end();
+  for (; assert_it != assert_it_end; ++assert_it)
+  {
+    collectTerms(*assert_it, termSet);
+  }
+
+  if (includeShared)
+  {
+    // Add terms that are shared terms
+    context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(),
+                                           shared_it_end = shared_terms_end();
+    for (; shared_it != shared_it_end; ++shared_it)
+    {
+      collectTerms(*shared_it, termSet);
+    }
+  }
+}
+
+void Theory::collectTerms(TNode n, std::set<Node>& termSet) const
+{
+  const std::set<Kind>& irrKinds =
+      d_theoryState->getModel()->getIrrelevantKinds();
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (termSet.find(cur) != termSet.end())
+    {
+      // already visited
+      continue;
+    }
+    Kind k = cur.getKind();
+    // only add to term set if a relevant kind
+    if (irrKinds.find(k) == irrKinds.end())
+    {
+      termSet.insert(cur);
+    }
+    // traverse owned terms, don't go under quantifiers
+    if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == d_id)
+        && !cur.isClosure())
+    {
+      visit.insert(visit.end(), cur.begin(), cur.end());
+    }
+  } while (!visit.empty());
+}
+
 bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 {
   return true;
@@ -620,7 +674,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 a857931a8..bde00b908 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -450,6 +450,11 @@ class Theory {
   Env& getEnv() const { return d_env; }
 
   /**
+   * Shorthand to access the options object.
+   */
+  const Options& options() const { return getEnv().getOptions(); }
+
+  /**
    * Get the SAT context associated to this Theory.
    */
   context::Context* getSatContext() const { return d_env.getContext(); }
@@ -639,6 +644,19 @@ class Theory {
    */
   virtual void computeRelevantTerms(std::set<Node>& termSet);
   /**
+   * Collect asserted terms for this theory and add them to  termSet.
+   *
+   * @param termSet The set to add terms to
+   * @param includeShared Whether to include the shared terms of the theory
+   */
+  void collectAssertedTerms(std::set<Node>& termSet,
+                            bool includeShared = true) const;
+  /**
+   * Helper function for collectAssertedTerms, adds all subterms
+   * belonging to this theory to termSet.
+   */
+  void collectTerms(TNode n, std::set<Node>& termSet) const;
+  /**
    * Collect model values, after equality information is added to the model.
    * The argument termSet is the set of relevant terms returned by
    * computeRelevantTerms.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 21c22586b..12d3fccfe 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -303,7 +303,16 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       // the atom should not have free variables
       Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
                       << std::endl;
-      Assert(!expr::hasFreeVar(preprocessed));
+      if (Configuration::isAssertionBuild())
+      {
+        std::unordered_set<Node> fvs;
+        expr::getFreeVariables(preprocessed, fvs);
+        if (!fvs.empty())
+        {
+          Unhandled() << "Preregistered term with free variable: "
+                      << preprocessed << ", fv=" << *fvs.begin();
+        }
+      }
       // should not have witness
       Assert(!expr::hasSubtermKind(kind::WITNESS, preprocessed));
 
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 58a66ef46..cc58347bf 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -47,6 +47,8 @@ class TheoryState
   context::UserContext* getUserContext() const;
   /** Get the environment */
   Env& getEnv() const { return d_env; }
+  /** Get the options */
+  const Options& options() const { return getEnv().getOptions(); }
   //-------------------------------------- equality information
   /** Is t registered as a term in the equality engine of this class? */
   virtual bool hasTerm(TNode a) const;
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 71742dfce..ad277cbb6 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -42,7 +42,6 @@ libcvc5_add_sources(
   iand.h
   index.cpp
   index.h
-  maybe.h
   ostream_util.cpp
   ostream_util.h
   poly_util.cpp
diff --git a/src/util/maybe.h b/src/util/maybe.h
deleted file mode 100644
index 838caa39e..000000000
--- a/src/util/maybe.h
+++ /dev/null
@@ -1,90 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Tim King, Mathias Preiner
- *
- * 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.
- * ****************************************************************************
- *
- * This provides a templated Maybe construct.
- *
- * This class provides a templated Maybe<T> construct.
- * This follows the rough pattern of the Maybe monad in haskell.
- * A Maybe is an algebraic type that is either Nothing | Just T
- *
- * T must support T() and operator=.
- *
- * This has a couple of uses:
- * - There is no reasonable value or particularly clean way to represent
- *   Nothing using a value of T
- * - High level of assurance that a value is not used before it is set.
- */
-#include "cvc5_public.h"
-
-#ifndef CVC5__UTIL__MAYBE_H
-#define CVC5__UTIL__MAYBE_H
-
-#include <ostream>
-
-#include "base/exception.h"
-
-namespace cvc5 {
-
-template <class T>
-class Maybe
-{
- public:
-  Maybe() : d_just(false), d_value(){}
-  Maybe(const T& val): d_just(true), d_value(val){}
-
-  Maybe& operator=(const T& v){
-    d_just = true;
-    d_value = v;
-    return *this;
-  }
-
-  inline bool nothing() const { return !d_just; }
-  inline bool just() const { return d_just; }
-  explicit operator bool() const noexcept { return just(); }
-
-  void clear() {
-    if(just()){
-      d_just = false;
-      d_value = T();
-    }
-  }
-
-  const T& value() const
-  {
-    if (nothing())
-    {
-      throw Exception("Maybe::value() requires the maybe to be set.");
-    }
-    return d_value;
-  }
-
- private:
-  bool d_just;
-  T d_value;
-};
-
-template <class T>
-inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){
-  out << "{";
-  if(m.nothing()){
-    out << "Nothing";
-  }else{
-    out << "Just ";
-    out << m.value();
-  }
-  out << "}";
-  return out;
-}
-
-}  // namespace cvc5
-
-#endif /* CVC5__UTIL__MAYBE_H */
diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp
index 133cd00a3..7a5ae714e 100644
--- a/src/util/poly_util.cpp
+++ b/src/util/poly_util.cpp
@@ -23,7 +23,6 @@
 #include <sstream>
 
 #include "base/check.h"
-#include "maybe.h"
 #include "util/integer.h"
 #include "util/rational.h"
 #include "util/real_algebraic_number.h"
@@ -157,7 +156,7 @@ poly::Rational toRational(const Rational& r)
 #endif
 }
 
-Maybe<poly::DyadicRational> toDyadicRational(const Rational& r)
+std::optional<poly::DyadicRational> toDyadicRational(const Rational& r)
 {
   Integer den = r.getDenominator();
   if (den.isOne())
@@ -170,10 +169,10 @@ Maybe<poly::DyadicRational> toDyadicRational(const Rational& r)
     // It's a dyadic rational.
     return div_2exp(poly::DyadicRational(toInteger(r.getNumerator())), exp - 1);
   }
-  return Maybe<poly::DyadicRational>();
+  return std::optional<poly::DyadicRational>();
 }
 
-Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r)
+std::optional<poly::DyadicRational> toDyadicRational(const poly::Rational& r)
 {
   poly::Integer den = denominator(r);
   if (den == poly::Integer(1))
@@ -187,7 +186,7 @@ Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r)
     // It's a dyadic rational.
     return div_2exp(poly::DyadicRational(numerator(r)), size);
   }
-  return Maybe<poly::DyadicRational>();
+  return std::optional<poly::DyadicRational>();
 }
 
 poly::Rational approximateToDyadic(const poly::Rational& r,
@@ -212,8 +211,8 @@ poly::AlgebraicNumber toPolyRanWithRefinement(poly::UPolynomial&& p,
                                               const Rational& lower,
                                               const Rational& upper)
 {
-  Maybe<poly::DyadicRational> ml = toDyadicRational(lower);
-  Maybe<poly::DyadicRational> mu = toDyadicRational(upper);
+  std::optional<poly::DyadicRational> ml = toDyadicRational(lower);
+  std::optional<poly::DyadicRational> mu = toDyadicRational(upper);
   if (ml && mu)
   {
     return poly::AlgebraicNumber(std::move(p),
diff --git a/src/util/poly_util.h b/src/util/poly_util.h
index b33710fce..f8c430bc2 100644
--- a/src/util/poly_util.h
+++ b/src/util/poly_util.h
@@ -18,9 +18,9 @@
 #ifndef CVC5__POLY_UTIL_H
 #define CVC5__POLY_UTIL_H
 
+#include <optional>
 #include <vector>
 
-#include "maybe.h"
 #include "util/integer.h"
 #include "util/rational.h"
 #include "util/real_algebraic_number.h"
@@ -66,12 +66,12 @@ poly::Rational toRational(const Rational& r);
  * Converts a cvc5::Rational to a poly::DyadicRational. If the input is not
  * dyadic, no result is produced.
  */
-Maybe<poly::DyadicRational> toDyadicRational(const Rational& r);
+std::optional<poly::DyadicRational> toDyadicRational(const Rational& r);
 /**
  * Converts a poly::Rational to a poly::DyadicRational. If the input is not
  * dyadic, no result is produced.
  */
-Maybe<poly::DyadicRational> toDyadicRational(const poly::Rational& r);
+std::optional<poly::DyadicRational> toDyadicRational(const poly::Rational& r);
 
 /**
  * Iteratively approximates a poly::Rational by a dyadic poly::Rational.
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 728b2d97e..033e53e95 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -99,7 +99,7 @@ int Rational::absCmp(const Rational& q) const{
   }
 }
 
-Maybe<Rational> Rational::fromDouble(double d)
+std::optional<Rational> Rational::fromDouble(double d)
 {
   try{
     cln::cl_DF fromD = d;
@@ -107,11 +107,11 @@ Maybe<Rational> Rational::fromDouble(double d)
     q.d_value = cln::rationalize(fromD);
     return q;
   }catch(cln::floating_point_underflow_exception& fpue){
-    return Maybe<Rational>();
+    return std::optional<Rational>();
   }catch(cln::floating_point_nan_exception& fpne){
-    return Maybe<Rational>();
+    return std::optional<Rational>();
   }catch(cln::floating_point_overflow_exception& fpoe){
-    return Maybe<Rational>();
+    return std::optional<Rational>();
   }
 }
 
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 67e73f7e9..f1b6022cf 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -27,13 +27,13 @@
 #include <cln/rational_io.h>
 #include <cln/real.h>
 
+#include <optional>
 #include <sstream>
 #include <string>
 
 #include "base/exception.h"
 #include "cvc5_export.h"  // remove when Cvc language support is removed
 #include "util/integer.h"
-#include "util/maybe.h"
 
 namespace cvc5 {
 
@@ -190,7 +190,7 @@ class CVC5_EXPORT Rational
   Integer getDenominator() const { return Integer(cln::denominator(d_value)); }
 
   /** Return an exact rational for a double d. */
-  static Maybe<Rational> fromDouble(double d);
+  static std::optional<Rational> fromDouble(double d);
 
   /**
    * Get a double representation of this Rational, which is
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index 0997b8b09..c68e15e27 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -85,7 +85,7 @@ int Rational::absCmp(const Rational& q) const{
 
 
 /** Return an exact rational for a double d. */
-Maybe<Rational> Rational::fromDouble(double d)
+std::optional<Rational> Rational::fromDouble(double d)
 {
   using namespace std;
   if(isfinite(d)){
@@ -93,7 +93,7 @@ Maybe<Rational> Rational::fromDouble(double d)
     mpq_set_d(q.d_value.get_mpq_t(), d);
     return q;
   }
-  return Maybe<Rational>();
+  return std::optional<Rational>();
 }
 
 }  // namespace cvc5
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index fd7492a87..b3c876533 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -20,12 +20,12 @@
 
 #include <gmp.h>
 
+#include <optional>
 #include <string>
 
 #include "cvc5_export.h"  // remove when Cvc language support is removed
 #include "util/gmp_util.h"
 #include "util/integer.h"
-#include "util/maybe.h"
 
 namespace cvc5 {
 
@@ -164,7 +164,7 @@ class CVC5_EXPORT Rational
    */
   Integer getDenominator() const { return Integer(d_value.get_den()); }
 
-  static Maybe<Rational> fromDouble(double d);
+  static std::optional<Rational> fromDouble(double d);
 
   /**
    * Get a double representation of this Rational, which is
diff --git a/src/util/utility.h b/src/util/utility.h
index 3958ff166..9126d3e25 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -21,6 +21,7 @@
 #include <algorithm>
 #include <fstream>
 #include <memory>
+#include <optional>
 #include <string>
 
 namespace cvc5 {
@@ -61,6 +62,31 @@ void container_to_stream(std::ostream& out,
 }
 
 /**
+ * Generates a string representation of std::optional and inserts it into a
+ * stream.
+ *
+ * @param out The stream
+ * @param m The value
+ * @return The stream
+ */
+template <class T>
+std::ostream& operator<<(std::ostream& out, const std::optional<T>& m)
+{
+  out << "{";
+  if (m)
+  {
+    out << "Just ";
+    out << *m;
+  }
+  else
+  {
+    out << "Nothing";
+  }
+  out << "}";
+  return out;
+}
+
+/**
  * Opens a new temporary file with a given filename pattern and returns an
  * fstream to it. The directory that the file is created in is either TMPDIR or
  * /tmp/ if TMPDIR is not set.
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2706dee8a..6f71e0993 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -910,6 +910,7 @@ set(regress_0_tests
   regress0/quantifiers/issue5645-dt-cm-spurious.smt2
   regress0/quantifiers/issue5693-prenex.smt2
   regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
+  regress0/quantifiers/issue6996-trivial-elim.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2
diff --git a/test/regress/regress0/quantifiers/issue6996-trivial-elim.smt2 b/test/regress/regress0/quantifiers/issue6996-trivial-elim.smt2
new file mode 100644
index 000000000..939044b4e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue6996-trivial-elim.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((@ 0)) (((V))))
+(declare-fun I (@ Int) Bool)
+(assert (forall ((v @) (i Int)) (! false :qid |outputbpl.122:24| :pattern ((I v i)))))
+(check-sat)
diff --git a/test/regress/regress0/use_approx/bug812_approx.smt2 b/test/regress/regress0/use_approx/bug812_approx.smt2
index 4b5af6710..45908e3dd 100644
--- a/test/regress/regress0/use_approx/bug812_approx.smt2
+++ b/test/regress/regress0/use_approx/bug812_approx.smt2
@@ -1,11 +1,10 @@
 ; REQUIRES: glpk
 ; COMMAND-LINE: --use-approx
-; EXPECT: unknown
 (set-logic UFNIA)
 (set-info :source "Reduced from regression 'bug812.smt2' using ddSMT to exercise GLPK")
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
-(set-info :status unknown)
+(set-info :status unsat)
 (declare-fun s (Int Int) Int)
 (declare-fun P (Int Int Int) Int)
 (declare-fun p (Int) Int)