Merge branch 'master' into rmNoInteractivePromptrmNoInteractivePrompt

22 files changed, 312 insertions, 253 deletions

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