From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 13 Sep 2021 23:14:54 +0000 (-0700)
Subject: Remove context getters from `TheoryState` (#7174)
X-Git-Tag: cvc5-1.0.0~1222
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a37f486c6e10b882a81474418e1d3f4ffdbd583c;p=cvc5.git

Remove context getters from `TheoryState` (#7174)

This removes TheoryState::getSatContext() and
TheoryState::getUserContext().
---

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index c975fbbfa..774c5db3f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -2125,7 +2125,7 @@ void TheoryArrays::conflict(TNode a, TNode b) {
 
 TheoryArrays::TheoryArraysDecisionStrategy::TheoryArraysDecisionStrategy(
     TheoryArrays* ta)
-    : d_ta(ta)
+    : DecisionStrategy(ta->d_env), d_ta(ta)
 {
 }
 void TheoryArrays::TheoryArraysDecisionStrategy::initialize() {}
diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index 510c8a29a..82d6a4a5d 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -20,7 +20,6 @@
 #ifndef CVC5__THEORY__BV__BV_SOLVER_H
 #define CVC5__THEORY__BV__BV_SOLVER_H
 
-#include "smt/env.h"
 #include "smt/env_obj.h"
 #include "theory/theory.h"
 
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index bb9cdb011..a8ae3b117 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -116,16 +116,16 @@ BVSolverBitblast::BVSolverBitblast(Env& env,
       d_bitblaster(new NodeBitblaster(env, s)),
       d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
       d_nullContext(new context::Context()),
-      d_bbFacts(s->getSatContext()),
-      d_bbInputFacts(s->getSatContext()),
-      d_assumptions(s->getSatContext()),
-      d_assertions(s->getSatContext()),
-      d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
+      d_bbFacts(context()),
+      d_bbInputFacts(context()),
+      d_assumptions(context()),
+      d_assertions(context()),
+      d_epg(pnm ? new EagerProofGenerator(pnm, userContext(), "")
                 : nullptr),
-      d_factLiteralCache(s->getSatContext()),
-      d_literalFactCache(s->getSatContext()),
+      d_factLiteralCache(context()),
+      d_literalFactCache(context()),
       d_propagate(options().bv.bitvectorPropagate),
-      d_resetNotify(new NotifyResetAssertions(s->getUserContext()))
+      d_resetNotify(new NotifyResetAssertions(userContext()))
 {
   if (pnm != nullptr)
   {
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index e8931acff..b9ae84f23 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -24,6 +24,7 @@
 #include "proof/eager_proof_generator.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
+#include "smt/env_obj.h"
 #include "theory/bv/bitblast/node_bitblaster.h"
 #include "theory/bv/bv_solver.h"
 #include "theory/bv/proof_checker.h"
diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h
index cc365e109..72b8b4f4d 100644
--- a/src/theory/bv/bv_solver_bitblast_internal.h
+++ b/src/theory/bv/bv_solver_bitblast_internal.h
@@ -19,6 +19,7 @@
 #ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H
 #define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H
 
+#include "smt/env_obj.h"
 #include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/bv/bv_solver.h"
 #include "theory/bv/proof_checker.h"
diff --git a/src/theory/bv/bv_solver_layered.cpp b/src/theory/bv/bv_solver_layered.cpp
index bf76ed2f9..682c556cc 100644
--- a/src/theory/bv/bv_solver_layered.cpp
+++ b/src/theory/bv/bv_solver_layered.cpp
@@ -37,8 +37,8 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-BVSolverLayered::BVSolverLayered(TheoryBV& bv,
-                                 Env& env,
+BVSolverLayered::BVSolverLayered(Env& env,
+                                 TheoryBV& bv,
                                  context::Context* c,
                                  context::UserContext* u,
                                  ProofNodeManager* pnm,
diff --git a/src/theory/bv/bv_solver_layered.h b/src/theory/bv/bv_solver_layered.h
index 325f2fc72..3b723b052 100644
--- a/src/theory/bv/bv_solver_layered.h
+++ b/src/theory/bv/bv_solver_layered.h
@@ -24,6 +24,7 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/context.h"
+#include "smt/env_obj.h"
 #include "theory/bv/bv_solver.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/bv/theory_bv.h"
@@ -57,8 +58,8 @@ class BVSolverLayered : public BVSolver
       d_subtheoryMap;
 
  public:
-  BVSolverLayered(TheoryBV& bv,
-                  Env& env,
+  BVSolverLayered(Env& env,
+                  TheoryBV& bv,
                   context::Context* c,
                   context::UserContext* u,
                   ProofNodeManager* pnm = nullptr,
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 397120ff1..ba90c669e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -46,17 +46,16 @@ TheoryBV::TheoryBV(Env& env,
   switch (options().bv.bvSolver)
   {
     case options::BVSolver::BITBLAST:
-      d_internal.reset(new BVSolverBitblast(d_env, &d_state, d_im, d_pnm));
+      d_internal.reset(new BVSolverBitblast(env, &d_state, d_im, d_pnm));
       break;
 
     case options::BVSolver::LAYERED:
       d_internal.reset(new BVSolverLayered(
-          *this, d_env, context(), userContext(), d_pnm, name));
+          env, *this, context(), userContext(), d_pnm, name));
       break;
 
     default:
-      AlwaysAssert(options().bv.bvSolver
-                   == options::BVSolver::BITBLAST_INTERNAL);
+      AlwaysAssert(options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL);
       d_internal.reset(
           new BVSolverBitblastInternal(d_env, &d_state, d_im, d_pnm));
   }
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index ed112e4ea..2411013b2 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -51,10 +51,10 @@ SygusExtension::SygusExtension(Env& env,
       d_im(im),
       d_tds(tds),
       d_ssb(tds),
-      d_testers(s.getSatContext()),
-      d_testers_exp(s.getSatContext()),
-      d_active_terms(s.getSatContext()),
-      d_currTermSize(s.getSatContext())
+      d_testers(context()),
+      d_testers_exp(context()),
+      d_active_terms(context()),
+      d_currTermSize(context())
 {
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -1325,11 +1325,8 @@ void SygusExtension::registerSizeTerm(Node e)
         d_anchor_to_ag_strategy.find(e);
     if (itaas == d_anchor_to_ag_strategy.end())
     {
-      d_anchor_to_ag_strategy[e].reset(
-          new DecisionStrategySingleton("sygus_enum_active",
-                                        ag,
-                                        d_state.getSatContext(),
-                                        d_state.getValuation()));
+      d_anchor_to_ag_strategy[e].reset(new DecisionStrategySingleton(
+          d_env, "sygus_enum_active", ag, d_state.getValuation()));
     }
     d_im.getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE,
@@ -1411,7 +1408,7 @@ void SygusExtension::registerMeasureTerm( Node m ) {
       d_szinfo.find(m);
   if( it==d_szinfo.end() ){
     Trace("sygus-sb") << "Sygus : register measure term : " << m << std::endl;
-    d_szinfo[m].reset(new SygusSizeDecisionStrategy(d_im, m, d_state));
+    d_szinfo[m].reset(new SygusSizeDecisionStrategy(d_env, d_im, m, d_state));
     // register this as a decision strategy
     d_im.getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE, d_szinfo[m].get());
@@ -1748,8 +1745,8 @@ Node SygusExtension::getCurrentTemplate( Node n, std::map< TypeNode, int >& var_
 }
 
 SygusExtension::SygusSizeDecisionStrategy::SygusSizeDecisionStrategy(
-    InferenceManager& im, Node t, TheoryState& s)
-    : DecisionStrategyFmf(s.getSatContext(), s.getValuation()),
+    Env& env, InferenceManager& im, Node t, TheoryState& s)
+    : DecisionStrategyFmf(env, s.getValuation()),
       d_this(t),
       d_curr_search_size(0),
       d_im(im)
diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h
index 5860dca99..c7a9e7893 100644
--- a/src/theory/datatypes/sygus_extension.h
+++ b/src/theory/datatypes/sygus_extension.h
@@ -555,7 +555,10 @@ private:
   class SygusSizeDecisionStrategy : public DecisionStrategyFmf
   {
    public:
-    SygusSizeDecisionStrategy(InferenceManager& im, Node t, TheoryState& s);
+    SygusSizeDecisionStrategy(Env& env,
+                              InferenceManager& im,
+                              Node t,
+                              TheoryState& s);
     /** the measure term */
     Node d_this;
     /**
diff --git a/src/theory/decision_strategy.cpp b/src/theory/decision_strategy.cpp
index dabfb55bb..7c932177a 100644
--- a/src/theory/decision_strategy.cpp
+++ b/src/theory/decision_strategy.cpp
@@ -23,11 +23,11 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace theory {
 
-DecisionStrategyFmf::DecisionStrategyFmf(context::Context* satContext,
-                                         Valuation valuation)
-    : d_valuation(valuation),
-      d_has_curr_literal(false, satContext),
-      d_curr_literal(0, satContext)
+DecisionStrategyFmf::DecisionStrategyFmf(Env& env, Valuation valuation)
+    : DecisionStrategy(env),
+      d_valuation(valuation),
+      d_has_curr_literal(false, context()),
+      d_curr_literal(0, context())
 {
 }
 
@@ -127,12 +127,11 @@ Node DecisionStrategyFmf::getLiteral(unsigned n)
   return ret;
 }
 
-DecisionStrategySingleton::DecisionStrategySingleton(
-    const char* name,
-    Node lit,
-    context::Context* satContext,
-    Valuation valuation)
-    : DecisionStrategyFmf(satContext, valuation), d_name(name), d_literal(lit)
+DecisionStrategySingleton::DecisionStrategySingleton(Env& env,
+                                                     const char* name,
+                                                     Node lit,
+                                                     Valuation valuation)
+    : DecisionStrategyFmf(env, valuation), d_name(name), d_literal(lit)
 {
 }
 
diff --git a/src/theory/decision_strategy.h b/src/theory/decision_strategy.h
index 8b5f75108..fc2975137 100644
--- a/src/theory/decision_strategy.h
+++ b/src/theory/decision_strategy.h
@@ -21,6 +21,7 @@
 
 #include "context/cdo.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/valuation.h"
 
 namespace cvc5 {
@@ -29,10 +30,10 @@ namespace theory {
 /**
  * Virtual base class for decision strategies.
  */
-class DecisionStrategy
+class DecisionStrategy : protected EnvObj
 {
  public:
-  DecisionStrategy() {}
+  DecisionStrategy(Env& env) : EnvObj(env) {}
   virtual ~DecisionStrategy() {}
   /**
    * Initalize this strategy, This is called once per satisfiability call by
@@ -68,7 +69,7 @@ class DecisionStrategy
 class DecisionStrategyFmf : public DecisionStrategy
 {
  public:
-  DecisionStrategyFmf(context::Context* satContext, Valuation valuation);
+  DecisionStrategyFmf(Env& env, Valuation valuation);
   virtual ~DecisionStrategyFmf() {}
   /** initialize */
   void initialize() override;
@@ -119,9 +120,9 @@ class DecisionStrategyFmf : public DecisionStrategy
 class DecisionStrategySingleton : public DecisionStrategyFmf
 {
  public:
-  DecisionStrategySingleton(const char* name,
+  DecisionStrategySingleton(Env& env,
+                            const char* name,
                             Node lit,
-                            context::Context* satContext,
                             Valuation valuation);
   /**
    * Make the n^th literal of this strategy. This method returns d_literal if
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 8334cc248..1ccfd8ede 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -56,7 +56,7 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env,
       d_irew(new InstRewriterCegqi(this)),
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
-      d_added_cbqi_lemma(qs.getUserContext()),
+      d_added_cbqi_lemma(userContext()),
       d_vtsCache(new VtsTermCache(qim)),
       d_bv_invert(nullptr),
       d_small_const_multiplier(
@@ -168,10 +168,8 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
     DecisionStrategy* dlds = nullptr;
     if (itds == d_dstrat.end())
     {
-      d_dstrat[q].reset(new DecisionStrategySingleton("CexLiteral",
-                                                      ceLit,
-                                                      d_qstate.getSatContext(),
-                                                      d_qstate.getValuation()));
+      d_dstrat[q].reset(new DecisionStrategySingleton(
+          d_env, "CexLiteral", ceLit, d_qstate.getValuation()));
       dlds = d_dstrat[q].get();
     }
     else
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index f9625d7ac..da8727c12 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -167,7 +167,7 @@ ConjectureGenerator::EqcInfo* ConjectureGenerator::getOrMakeEqcInfo( TNode n, bo
   if( eqc_i!=d_eqc_info.end() ){
     return eqc_i->second;
   }else if( doMake ){
-    EqcInfo* ei = new EqcInfo(d_qstate.getSatContext());
+    EqcInfo* ei = new EqcInfo(context());
     d_eqc_info[n] = ei;
     return ei;
   }else{
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 92ec1e452..30d223b2a 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -33,7 +33,7 @@ EqualityQuery::EqualityQuery(Env& env, QuantifiersState& qs, FirstOrderModel* m)
     : QuantifiersUtil(env),
       d_qstate(qs),
       d_model(m),
-      d_eqi_counter(qs.getSatContext()),
+      d_eqi_counter(context()),
       d_reset_count(0)
 {
 }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 841177a7f..cfd903646 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -46,11 +46,12 @@ FirstOrderModel::FirstOrderModel(Env& env,
                                  QuantifiersState& qs,
                                  QuantifiersRegistry& qr,
                                  TermRegistry& tr)
-    : d_model(nullptr),
+    : EnvObj(env),
+      d_model(nullptr),
       d_qreg(qr),
       d_treg(tr),
       d_eq_query(env, qs, this),
-      d_forall_asserts(qs.getSatContext()),
+      d_forall_asserts(context()),
       d_forallRlvComputed(false)
 {
 }
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 05bdcbee6..526bbe10b 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -19,6 +19,7 @@
 #define CVC5__FIRST_ORDER_MODEL_H
 
 #include "context/cdlist.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_model.h"
@@ -36,7 +37,7 @@ class TermRegistry;
 class QuantifiersRegistry;
 
 // TODO (#1301) : document and refactor this class
-class FirstOrderModel
+class FirstOrderModel : protected EnvObj
 {
  public:
   FirstOrderModel(Env& env,
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index b04391db3..4a3e13dd0 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -37,12 +37,10 @@ using namespace cvc5::theory::quantifiers;
 using namespace cvc5::kind;
 
 BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
-    Node r,
-    context::Context* c,
-    context::Context* u,
-    Valuation valuation,
-    bool isProxy)
-    : DecisionStrategyFmf(c, valuation), d_range(r), d_ranges_proxied(u)
+    Env& env, Node r, Valuation valuation, bool isProxy)
+    : DecisionStrategyFmf(env, valuation),
+      d_range(r),
+      d_ranges_proxied(userContext())
 {
   if( options::fmfBoundLazy() ){
     SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
@@ -514,12 +512,8 @@ void BoundedIntegers::checkOwnership(Node f)
           {
             Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;
             d_ranges.push_back( r );
-            d_rms[r].reset(
-                new IntRangeDecisionHeuristic(r,
-                                              d_qstate.getSatContext(),
-                                              d_qstate.getUserContext(),
-                                              d_qstate.getValuation(),
-                                              isProxy));
+            d_rms[r].reset(new IntRangeDecisionHeuristic(
+                d_env, r, d_qstate.getValuation(), isProxy));
             dm->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE,
                                  d_rms[r].get());
           }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 8c468c1de..2c3a86fc7 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -100,9 +100,8 @@ private:
  class IntRangeDecisionHeuristic : public DecisionStrategyFmf
  {
   public:
-   IntRangeDecisionHeuristic(Node r,
-                             context::Context* c,
-                             context::Context* u,
+   IntRangeDecisionHeuristic(Env& env,
+                             Node r,
                              Valuation valuation,
                              bool isProxy);
    /** make the n^th literal of this strategy */
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index ba9ea9152..a4107564e 100644
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -189,16 +189,18 @@ CDInstMatchTrie::~CDInstMatchTrie()
   d_data.clear();
 }
 
-bool CDInstMatchTrie::existsInstMatch(quantifiers::QuantifiersState& qs,
+bool CDInstMatchTrie::existsInstMatch(context::Context* context,
+                                      quantifiers::QuantifiersState& qs,
                                       Node q,
                                       const std::vector<Node>& m,
                                       bool modEq,
                                       unsigned index)
 {
-  return !addInstMatch(qs, q, m, modEq, index, true);
+  return !addInstMatch(context, qs, q, m, modEq, index, true);
 }
 
-bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
+bool CDInstMatchTrie::addInstMatch(context::Context* context,
+                                   quantifiers::QuantifiersState& qs,
                                    Node f,
                                    const std::vector<Node>& m,
                                    bool modEq,
@@ -226,7 +228,8 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
   std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n);
   if (it != d_data.end())
   {
-    bool ret = it->second->addInstMatch(qs, f, m, modEq, index + 1, onlyExist);
+    bool ret =
+        it->second->addInstMatch(context, qs, f, m, modEq, index + 1, onlyExist);
     if (!onlyExist || !ret)
     {
       return reset || ret;
@@ -246,7 +249,8 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
           std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en);
           if (itc != d_data.end())
           {
-            if (itc->second->addInstMatch(qs, f, m, modEq, index + 1, true))
+            if (itc->second->addInstMatch(
+                    context, qs, f, m, modEq, index + 1, true))
             {
               return false;
             }
@@ -259,10 +263,10 @@ bool CDInstMatchTrie::addInstMatch(quantifiers::QuantifiersState& qs,
 
   if (!onlyExist)
   {
-    CDInstMatchTrie* imt = new CDInstMatchTrie(qs.getUserContext());
+    CDInstMatchTrie* imt = new CDInstMatchTrie(context);
     Assert(d_data.find(n) == d_data.end());
     d_data[n] = imt;
-    imt->addInstMatch(qs, f, m, modEq, index + 1, false);
+    imt->addInstMatch(context, qs, f, m, modEq, index + 1, false);
   }
   return true;
 }
diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index 83bd8d3b1..5ddc299af 100644
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -23,6 +23,7 @@
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace theory {
@@ -131,7 +132,8 @@ class CDInstMatchTrie
    * equalities in the equality engine of qs.
    * It additionally takes a context c, for which the entry is valid in.
    */
-  bool existsInstMatch(QuantifiersState& qs,
+  bool existsInstMatch(context::Context* context,
+                       QuantifiersState& qs,
                        Node q,
                        const std::vector<Node>& m,
                        bool modEq = false,
@@ -145,7 +147,8 @@ class CDInstMatchTrie
    * equalities in the equality engine of qs.
    * It additionally takes a context c, for which the entry is valid in.
    */
-  bool addInstMatch(QuantifiersState& qs,
+  bool addInstMatch(context::Context* context,
+                    QuantifiersState& qs,
                     Node q,
                     const std::vector<Node>& m,
                     bool modEq = false,
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index f0af73832..2a3974d49 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -54,11 +54,10 @@ Instantiate::Instantiate(Env& env,
       d_qreg(qr),
       d_treg(tr),
       d_pnm(pnm),
-      d_insts(qs.getUserContext()),
-      d_c_inst_match_trie_dom(qs.getUserContext()),
-      d_pfInst(
-          pnm ? new CDProof(pnm, qs.getUserContext(), "Instantiate::pfInst")
-              : nullptr)
+      d_insts(userContext()),
+      d_c_inst_match_trie_dom(userContext()),
+      d_pfInst(pnm ? new CDProof(pnm, userContext(), "Instantiate::pfInst")
+                   : nullptr)
 {
 }
 
@@ -507,7 +506,7 @@ bool Instantiate::existsInstantiation(Node q,
     std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
     if (it != d_c_inst_match_trie.end())
     {
-      return it->second->existsInstMatch(d_qstate, q, terms, modEq);
+      return it->second->existsInstMatch(userContext(), d_qstate, q, terms, modEq);
     }
   }
   else
@@ -594,10 +593,10 @@ bool Instantiate::recordInstantiationInternal(Node q, std::vector<Node>& terms)
     const auto res = d_c_inst_match_trie.insert({q, nullptr});
     if (res.second)
     {
-      res.first->second = new CDInstMatchTrie(d_qstate.getUserContext());
+      res.first->second = new CDInstMatchTrie(userContext());
     }
     d_c_inst_match_trie_dom.insert(q);
-    return res.first->second->addInstMatch(d_qstate, q, terms);
+    return res.first->second->addInstMatch(userContext(), d_qstate, q, terms);
   }
   Trace("inst-add-debug") << "Adding into inst trie" << std::endl;
   return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms);
@@ -750,7 +749,7 @@ InstLemmaList* Instantiate::getOrMkInstLemmaList(TNode q)
     return it->second.get();
   }
   std::shared_ptr<InstLemmaList> ill =
-      std::make_shared<InstLemmaList>(d_qstate.getUserContext());
+      std::make_shared<InstLemmaList>(userContext());
   d_insts.insert(q, ill);
   return ill.get();
 }
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 983eee9ae..1de60422f 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1859,7 +1859,7 @@ QuantConflictFind::QuantConflictFind(Env& env,
                                      QuantifiersRegistry& qr,
                                      TermRegistry& tr)
     : QuantifiersModule(env, qs, qim, qr, tr),
-      d_conflict(qs.getSatContext(), false),
+      d_conflict(context(), false),
       d_true(NodeManager::currentNM()->mkConst<bool>(true)),
       d_false(NodeManager::currentNM()->mkConst<bool>(false)),
       d_effort(EFFORT_INVALID)
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 905424107..db07d07d0 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -33,8 +33,7 @@ QuantDSplit::QuantDSplit(Env& env,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr)
-    : QuantifiersModule(env, qs, qim, qr, tr),
-      d_added_split(qs.getUserContext())
+    : QuantifiersModule(env, qs, qim, qr, tr), d_added_split(userContext())
 {
 }
 
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index b2a08c249..20987b02e 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -31,7 +31,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager(
     ProofNodeManager* pnm)
     : InferenceManagerBuffered(env, t, state, pnm, "theory::quantifiers::"),
       d_instantiate(new Instantiate(env, state, *this, qr, tr, pnm)),
-      d_skolemize(new Skolemize(state, tr, pnm))
+      d_skolemize(new Skolemize(env, state, tr, pnm))
 {
 }
 
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 23b66b1de..bb0fa3899 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -35,16 +35,18 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-Skolemize::Skolemize(QuantifiersState& qs,
+Skolemize::Skolemize(Env& env,
+                     QuantifiersState& qs,
                      TermRegistry& tr,
                      ProofNodeManager* pnm)
-    : d_qstate(qs),
+    : EnvObj(env),
+      d_qstate(qs),
       d_treg(tr),
-      d_skolemized(qs.getUserContext()),
+      d_skolemized(userContext()),
       d_pnm(pnm),
-      d_epg(pnm == nullptr ? nullptr
-                           : new EagerProofGenerator(
-                                 pnm, qs.getUserContext(), "Skolemize::epg"))
+      d_epg(pnm == nullptr
+                ? nullptr
+                : new EagerProofGenerator(pnm, userContext(), "Skolemize::epg"))
 {
 }
 
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index fbb79f5d2..294ad0084 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -26,6 +26,7 @@
 #include "expr/type_node.h"
 #include "proof/eager_proof_generator.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -63,12 +64,15 @@ class TermRegistry;
  * default and can be enabled by option:
  *   --quant-ind
  */
-class Skolemize
+class Skolemize : protected EnvObj
 {
   typedef context::CDHashMap<Node, Node> NodeNodeMap;
 
  public:
-  Skolemize(QuantifiersState& qs, TermRegistry& tr, ProofNodeManager* pnm);
+  Skolemize(Env& env,
+            QuantifiersState& qs,
+            TermRegistry& tr,
+            ProofNodeManager* pnm);
   ~Skolemize() {}
   /** skolemize quantified formula q
    * If the return value ret of this function is non-null, then ret is a trust
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 871a85fbd..6b260bb81 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -409,7 +409,7 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
     QuantifiersInferenceManager& qim,
     TermDbSygus* tds,
     SynthConjecture* parent)
-    : DecisionStrategyFmf(qs.getSatContext(), qs.getValuation()),
+    : DecisionStrategyFmf(env, qs.getValuation()),
       d_qim(qim),
       d_tds(tds),
       d_parent(parent)
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index da021227a..22ba879d7 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -241,11 +241,8 @@ void SynthConjecture::assign(Node q)
   }
 
   // register the strategy
-  d_feasible_strategy.reset(
-      new DecisionStrategySingleton("sygus_feasible",
-                                    d_feasible_guard,
-                                    d_qstate.getSatContext(),
-                                    d_qstate.getValuation()));
+  d_feasible_strategy.reset(new DecisionStrategySingleton(
+      d_env, "sygus_feasible", d_feasible_guard, d_qstate.getValuation()));
   d_qim.getDecisionManager()->registerStrategy(
       DecisionManager::STRAT_QUANT_SYGUS_FEASIBLE, d_feasible_strategy.get());
   // this must be called, both to ensure that the feasible guard is
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 4da273cd9..64bc578a5 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -529,7 +529,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
    */
   Assert(d_dstrat.find(q) == d_dstrat.end());
   DecisionStrategy* ds = new DecisionStrategySingleton(
-      "CeLiteral", lit, d_qstate.getSatContext(), d_qstate.getValuation());
+      d_env, "CeLiteral", lit, d_qstate.getValuation());
 
   d_dstrat[q].reset(ds);
   d_qim.getDecisionManager()->registerStrategy(
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 6aa2a816a..7126d3567 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -43,13 +43,12 @@ TermDb::TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr)
       d_qim(nullptr),
       d_qreg(qr),
       d_termsContext(),
-      d_termsContextUse(options::termDbCd() ? qs.getSatContext()
-                                            : &d_termsContext),
+      d_termsContextUse(options::termDbCd() ? context() : &d_termsContext),
       d_processed(d_termsContextUse),
       d_typeMap(d_termsContextUse),
       d_ops(d_termsContextUse),
       d_opMap(d_termsContextUse),
-      d_inactive_map(qs.getSatContext())
+      d_inactive_map(context())
 {
   d_consistent_ee = true;
   d_true = NodeManager::currentNM()->mkConst(true);
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index 98618f3f7..ab999ad9b 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -33,8 +33,8 @@ TermRegistry::TermRegistry(Env& env,
                            QuantifiersState& qs,
                            QuantifiersRegistry& qr)
     : EnvObj(env),
-      d_presolve(qs.getUserContext(), true),
-      d_presolveCache(qs.getUserContext()),
+      d_presolve(userContext(), true),
+      d_presolveCache(userContext()),
       d_termEnum(new TermEnumeration),
       d_termPools(new TermPools(env, qs)),
       d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr)
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5f914484a..b713dbec1 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -59,8 +59,8 @@ QuantifiersEngine::QuantifiersEngine(
       d_qreg(qr),
       d_treg(tr),
       d_model(nullptr),
-      d_quants_prereg(qs.getUserContext()),
-      d_quants_red(qs.getUserContext()),
+      d_quants_prereg(userContext()),
+      d_quants_red(userContext()),
       d_numInstRoundsLemma(0)
 {
   Trace("quant-init-debug")
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index e19e90634..d28bae12a 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -467,7 +467,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
         << std::endl;
     Node g = sm->mkDummySkolem("G", nm->booleanType());
     d_neg_guard_strategy[g].reset(new DecisionStrategySingleton(
-        "sep_neg_guard", g, context(), getValuation()));
+        d_env, "sep_neg_guard", g, getValuation()));
     DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get();
     d_im.getDecisionManager()->registerStrategy(
         DecisionManager::STRAT_SEP_NEG_GUARD, ds);
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 39b1fcca9..184214724 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -35,13 +35,15 @@ namespace cvc5 {
 namespace theory {
 namespace sets {
 
-CardinalityExtension::CardinalityExtension(SolverState& s,
+CardinalityExtension::CardinalityExtension(Env& env,
+                                           SolverState& s,
                                            InferenceManager& im,
                                            TermRegistry& treg)
-    : d_state(s),
+    : EnvObj(env),
+      d_state(s),
       d_im(im),
       d_treg(treg),
-      d_card_processed(s.getUserContext()),
+      d_card_processed(userContext()),
       d_finite_type_constants_processed(false)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h
index bddcfaf1b..d3f9971d6 100644
--- a/src/theory/sets/cardinality_extension.h
+++ b/src/theory/sets/cardinality_extension.h
@@ -20,6 +20,7 @@
 
 #include "context/cdhashset.h"
 #include "context/context.h"
+#include "smt/env_obj.h"
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/solver_state.h"
 #include "theory/sets/term_registry.h"
@@ -60,7 +61,7 @@ namespace sets {
  * normal forms, where the normal form for Set terms is a set of (equivalence
  * class representatives of) Venn regions that do not contain the empty set.
  */
-class CardinalityExtension
+class CardinalityExtension : protected EnvObj
 {
   typedef context::CDHashSet<Node> NodeSet;
 
@@ -69,7 +70,8 @@ class CardinalityExtension
    * Constructs a new instance of the cardinality solver w.r.t. the provided
    * contexts.
    */
-  CardinalityExtension(SolverState& s,
+  CardinalityExtension(Env& env,
+                       SolverState& s,
                        InferenceManager& im,
                        TermRegistry& treg);
 
diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp
index be8e5858e..f1fe1c6b2 100644
--- a/src/theory/sets/term_registry.cpp
+++ b/src/theory/sets/term_registry.cpp
@@ -25,14 +25,16 @@ namespace cvc5 {
 namespace theory {
 namespace sets {
 
-TermRegistry::TermRegistry(SolverState& state,
+TermRegistry::TermRegistry(Env& env,
+                           SolverState& state,
                            InferenceManager& im,
                            SkolemCache& skc,
                            ProofNodeManager* pnm)
-    : d_im(im),
+    : EnvObj(env),
+      d_im(im),
       d_skCache(skc),
-      d_proxy(state.getUserContext()),
-      d_proxy_to_term(state.getUserContext()),
+      d_proxy(userContext()),
+      d_proxy_to_term(userContext()),
       d_epg(
           pnm ? new EagerProofGenerator(pnm, nullptr, "sets::TermRegistry::epg")
               : nullptr)
diff --git a/src/theory/sets/term_registry.h b/src/theory/sets/term_registry.h
index f88596ffe..e0a03cef4 100644
--- a/src/theory/sets/term_registry.h
+++ b/src/theory/sets/term_registry.h
@@ -23,6 +23,7 @@
 
 #include "context/cdhashmap.h"
 #include "proof/eager_proof_generator.h"
+#include "smt/env_obj.h"
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/skolem_cache.h"
 #include "theory/sets/solver_state.h"
@@ -35,12 +36,13 @@ namespace sets {
  * Term registry, the purpose of this class is to maintain a database of
  * commonly used terms, and mappings from sets to their "proxy variables".
  */
-class TermRegistry
+class TermRegistry : protected EnvObj
 {
   typedef context::CDHashMap<Node, Node> NodeMap;
 
  public:
-  TermRegistry(SolverState& state,
+  TermRegistry(Env& env,
+               SolverState& state,
                InferenceManager& im,
                SkolemCache& skc,
                ProofNodeManager* pnm);
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 8073b4c2a..2164c26b0 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -51,9 +51,9 @@ TheorySetsPrivate::TheorySetsPrivate(Env& env,
       d_state(state),
       d_im(im),
       d_skCache(skc),
-      d_treg(state, im, skc, pnm),
-      d_rels(new TheorySetsRels(state, im, skc, d_treg)),
-      d_cardSolver(new CardinalityExtension(state, im, d_treg)),
+      d_treg(d_env, state, im, skc, pnm),
+      d_rels(new TheorySetsRels(d_env, state, im, skc, d_treg)),
+      d_cardSolver(new CardinalityExtension(d_env, state, im, d_treg)),
       d_rels_enabled(false),
       d_card_enabled(false)
 {
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 65f5cedf5..f6ea88b75 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -34,15 +34,17 @@ typedef std::map< Node, std::map< kind::Kind_t, std::vector< Node > > >::iterato
 typedef std::map<Node, std::map<Node, std::unordered_set<Node> > >::iterator
     TC_IT;
 
-TheorySetsRels::TheorySetsRels(SolverState& s,
+TheorySetsRels::TheorySetsRels(Env& env,
+                               SolverState& s,
                                InferenceManager& im,
                                SkolemCache& skc,
                                TermRegistry& treg)
-    : d_state(s),
+    : EnvObj(env),
+      d_state(s),
       d_im(im),
       d_skCache(skc),
       d_treg(treg),
-      d_shared_terms(s.getUserContext())
+      d_shared_terms(userContext())
 {
   d_trueNode = NodeManager::currentNM()->mkConst(true);
   d_falseNode = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 89514c641..560f47482 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -20,6 +20,7 @@
 
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
+#include "smt/env_obj.h"
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/rels_utils.h"
 #include "theory/sets/solver_state.h"
@@ -59,13 +60,15 @@ public:
  * extension of the theory of sets. That is, it shares many components of the
  * TheorySets object which owns it.
  */
-class TheorySetsRels {
+class TheorySetsRels : protected EnvObj
+{
   typedef context::CDList<Node> NodeList;
   typedef context::CDHashSet<Node> NodeSet;
   typedef context::CDHashMap<Node, Node> NodeMap;
 
  public:
-  TheorySetsRels(SolverState& s,
+  TheorySetsRels(Env& env,
+                 SolverState& s,
                  InferenceManager& im,
                  SkolemCache& skc,
                  TermRegistry& treg);
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 5e685576c..3c825e4ae 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -31,8 +31,8 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-BaseSolver::BaseSolver(SolverState& s, InferenceManager& im)
-    : d_state(s), d_im(im), d_congruent(s.getSatContext())
+BaseSolver::BaseSolver(Env& env, SolverState& s, InferenceManager& im)
+    : EnvObj(env), d_state(s), d_im(im), d_congruent(context())
 {
   d_false = NodeManager::currentNM()->mkConst(false);
   d_cardSize = utils::getAlphabetCardinality();
diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
index 6c423e3b8..27f9ec40d 100644
--- a/src/theory/strings/base_solver.h
+++ b/src/theory/strings/base_solver.h
@@ -21,6 +21,7 @@
 
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
+#include "smt/env_obj.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/inference_manager.h"
 #include "theory/strings/normal_form.h"
@@ -37,12 +38,12 @@ namespace strings {
  * current context, and techniques for inferring when equivalence classes
  * are equivalent to constants.
  */
-class BaseSolver
+class BaseSolver : protected EnvObj
 {
   using NodeSet = context::CDHashSet<Node>;
 
  public:
-  BaseSolver(SolverState& s, InferenceManager& im);
+  BaseSolver(Env& env, SolverState& s, InferenceManager& im);
   ~BaseSolver();
 
   //-----------------------inference steps
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index fb1d086a4..98a0e819c 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -37,15 +37,17 @@ namespace strings {
 
 CoreInferInfo::CoreInferInfo(InferenceId id) : d_infer(id), d_index(0), d_rev(false) {}
 
-CoreSolver::CoreSolver(SolverState& s,
+CoreSolver::CoreSolver(Env& env,
+                       SolverState& s,
                        InferenceManager& im,
                        TermRegistry& tr,
                        BaseSolver& bs)
-    : d_state(s),
+    : EnvObj(env),
+      d_state(s),
       d_im(im),
       d_termReg(tr),
       d_bsolver(bs),
-      d_nfPairs(s.getSatContext())
+      d_nfPairs(context())
 {
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h
index 4e8a0a96b..35d37ce12 100644
--- a/src/theory/strings/core_solver.h
+++ b/src/theory/strings/core_solver.h
@@ -21,6 +21,7 @@
 
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
+#include "smt/env_obj.h"
 #include "theory/strings/base_solver.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/inference_manager.h"
@@ -76,13 +77,14 @@ class CoreInferInfo
  * This implements techniques for handling (dis)equalities involving
  * string concatenation terms based on the procedure by Liang et al CAV 2014.
  */
-class CoreSolver
+class CoreSolver : protected EnvObj
 {
   friend class InferenceManager;
   using NodeIntMap = context::CDHashMap<Node, int>;
 
  public:
-  CoreSolver(SolverState& s,
+  CoreSolver(Env& env,
+             SolverState& s,
              InferenceManager& im,
              TermRegistry& tr,
              BaseSolver& bs);
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index d5b1b7088..86f4e48fd 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -29,7 +29,8 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-ExtfSolver::ExtfSolver(SolverState& s,
+ExtfSolver::ExtfSolver(Env& env,
+                       SolverState& s,
                        InferenceManager& im,
                        TermRegistry& tr,
                        StringsRewriter& rewriter,
@@ -37,7 +38,8 @@ ExtfSolver::ExtfSolver(SolverState& s,
                        CoreSolver& cs,
                        ExtTheory& et,
                        SequencesStatistics& statistics)
-    : d_state(s),
+    : EnvObj(env),
+      d_state(s),
       d_im(im),
       d_termReg(tr),
       d_rewriter(rewriter),
@@ -46,9 +48,9 @@ ExtfSolver::ExtfSolver(SolverState& s,
       d_extt(et),
       d_statistics(statistics),
       d_preproc(d_termReg.getSkolemCache(), &statistics.d_reductions),
-      d_hasExtf(s.getSatContext(), false),
-      d_extfInferCache(s.getSatContext()),
-      d_reduced(s.getUserContext())
+      d_hasExtf(context(), false),
+      d_extfInferCache(context()),
+      d_reduced(userContext())
 {
   d_extt.addFunctionKind(kind::STRING_SUBSTR);
   d_extt.addFunctionKind(kind::STRING_UPDATE);
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index 82b4f61ee..2a9ca2d45 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -23,6 +23,7 @@
 
 #include "context/cdo.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/ext_theory.h"
 #include "theory/strings/base_solver.h"
 #include "theory/strings/core_solver.h"
@@ -79,12 +80,13 @@ class ExtfInfoTmp
  * functions for the theory of strings using a combination of context-dependent
  * simplification (Reynolds et al CAV 2017) and lazy reductions.
  */
-class ExtfSolver
+class ExtfSolver : protected EnvObj
 {
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  ExtfSolver(SolverState& s,
+  ExtfSolver(Env& env,
+             SolverState& s,
              InferenceManager& im,
              TermRegistry& tr,
              StringsRewriter& rewriter,
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 18815c731..7d077059b 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -32,20 +32,22 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-RegExpSolver::RegExpSolver(SolverState& s,
+RegExpSolver::RegExpSolver(Env& env,
+                           SolverState& s,
                            InferenceManager& im,
                            SkolemCache* skc,
                            CoreSolver& cs,
                            ExtfSolver& es,
                            SequencesStatistics& stats)
-    : d_state(s),
+    : EnvObj(env),
+      d_state(s),
       d_im(im),
       d_csolver(cs),
       d_esolver(es),
       d_statistics(stats),
-      d_regexp_ucached(s.getUserContext()),
-      d_regexp_ccached(s.getSatContext()),
-      d_processed_memberships(s.getSatContext()),
+      d_regexp_ucached(userContext()),
+      d_regexp_ccached(context()),
+      d_processed_memberships(context()),
       d_regexp_opr(skc)
 {
   d_emptyString = NodeManager::currentNM()->mkConst(::cvc5::String(""));
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index 98e2449c5..1d617eb1e 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -19,15 +19,17 @@
 #define CVC5__THEORY__STRINGS__REGEXP_SOLVER_H
 
 #include <map>
+
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/strings/extf_solver.h"
 #include "theory/strings/inference_manager.h"
-#include "theory/strings/skolem_cache.h"
 #include "theory/strings/regexp_operation.h"
 #include "theory/strings/sequences_stats.h"
+#include "theory/strings/skolem_cache.h"
 #include "theory/strings/solver_state.h"
 #include "util/string.h"
 
@@ -35,7 +37,7 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-class RegExpSolver
+class RegExpSolver : protected EnvObj
 {
   typedef context::CDList<Node> NodeList;
   typedef context::CDHashMap<Node, bool> NodeBoolMap;
@@ -45,7 +47,8 @@ class RegExpSolver
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  RegExpSolver(SolverState& s,
+  RegExpSolver(Env& env,
+               SolverState& s,
                InferenceManager& im,
                SkolemCache* skc,
                CoreSolver& cs,
diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp
index 9bb6a2420..b1050f480 100644
--- a/src/theory/strings/strings_fmf.cpp
+++ b/src/theory/strings/strings_fmf.cpp
@@ -25,15 +25,8 @@ namespace cvc5 {
 namespace theory {
 namespace strings {
 
-StringsFmf::StringsFmf(context::Context* c,
-                       context::UserContext* u,
-                       Valuation valuation,
-                       TermRegistry& tr)
-    : d_sslds(nullptr),
-      d_satContext(c),
-      d_userContext(u),
-      d_valuation(valuation),
-      d_termReg(tr)
+StringsFmf::StringsFmf(Env& env, Valuation valuation, TermRegistry& tr)
+    : EnvObj(env), d_sslds(nullptr), d_valuation(valuation), d_termReg(tr)
 {
 }
 
@@ -41,8 +34,7 @@ StringsFmf::~StringsFmf() {}
 
 void StringsFmf::presolve()
 {
-  d_sslds.reset(new StringSumLengthDecisionStrategy(
-      d_satContext, d_userContext, d_valuation));
+  d_sslds.reset(new StringSumLengthDecisionStrategy(d_env, d_valuation));
   Trace("strings-dstrat-reg")
       << "presolve: register decision strategy." << std::endl;
   const NodeSet& ivars = d_termReg.getInputVars();
@@ -60,8 +52,8 @@ DecisionStrategy* StringsFmf::getDecisionStrategy() const
 }
 
 StringsFmf::StringSumLengthDecisionStrategy::StringSumLengthDecisionStrategy(
-    context::Context* c, context::UserContext* u, Valuation valuation)
-    : DecisionStrategyFmf(c, valuation), d_inputVarLsum(u)
+    Env& env, Valuation valuation)
+    : DecisionStrategyFmf(env, valuation), d_inputVarLsum(userContext())
 {
 }
 
diff --git a/src/theory/strings/strings_fmf.h b/src/theory/strings/strings_fmf.h
index 39ba6168a..6b09ba198 100644
--- a/src/theory/strings/strings_fmf.h
+++ b/src/theory/strings/strings_fmf.h
@@ -22,6 +22,7 @@
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/decision_strategy.h"
 #include "theory/strings/term_registry.h"
 #include "theory/valuation.h"
@@ -35,15 +36,12 @@ namespace strings {
  * This class manages the creation of a decision strategy that bounds the
  * sum of lengths of terms of type string.
  */
-class StringsFmf
+class StringsFmf : protected EnvObj
 {
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  StringsFmf(context::Context* c,
-             context::UserContext* u,
-             Valuation valuation,
-             TermRegistry& tr);
+  StringsFmf(Env& env, Valuation valuation, TermRegistry& tr);
   ~StringsFmf();
   /** presolve
    *
@@ -68,9 +66,7 @@ class StringsFmf
   class StringSumLengthDecisionStrategy : public DecisionStrategyFmf
   {
    public:
-    StringSumLengthDecisionStrategy(context::Context* c,
-                                    context::UserContext* u,
-                                    Valuation valuation);
+    StringSumLengthDecisionStrategy(Env& env, Valuation valuation);
     /** make literal */
     Node mkLiteral(unsigned i) override;
     /** identify */
@@ -95,10 +91,6 @@ class StringsFmf
   };
   /** an instance of the above class */
   std::unique_ptr<StringSumLengthDecisionStrategy> d_sslds;
-  /** The SAT search context for the theory of strings. */
-  context::Context* d_satContext;
-  /** The user level assertion context for the theory of strings. */
-  context::UserContext* d_userContext;
   /** The valuation object of theory of strings */
   Valuation d_valuation;
   /** The term registry of theory of strings */
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 1b77308d7..dd53adecc 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -40,25 +40,26 @@ struct StringsProxyVarAttributeId
 typedef expr::Attribute<StringsProxyVarAttributeId, bool>
     StringsProxyVarAttribute;
 
-TermRegistry::TermRegistry(SolverState& s,
+TermRegistry::TermRegistry(Env& env,
+                           SolverState& s,
                            SequencesStatistics& statistics,
                            ProofNodeManager* pnm)
-    : d_state(s),
+    : EnvObj(env),
+      d_state(s),
       d_im(nullptr),
       d_statistics(statistics),
       d_hasStrCode(false),
-      d_functionsTerms(s.getSatContext()),
-      d_inputVars(s.getUserContext()),
-      d_preregisteredTerms(s.getSatContext()),
-      d_registeredTerms(s.getUserContext()),
-      d_registeredTypes(s.getUserContext()),
-      d_proxyVar(s.getUserContext()),
-      d_lengthLemmaTermsCache(s.getUserContext()),
-      d_epg(pnm ? new EagerProofGenerator(
-                      pnm,
-                      s.getUserContext(),
-                      "strings::TermRegistry::EagerProofGenerator")
-                : nullptr)
+      d_functionsTerms(context()),
+      d_inputVars(userContext()),
+      d_preregisteredTerms(context()),
+      d_registeredTerms(userContext()),
+      d_registeredTypes(userContext()),
+      d_proxyVar(userContext()),
+      d_lengthLemmaTermsCache(userContext()),
+      d_epg(
+          pnm ? new EagerProofGenerator(
+              pnm, userContext(), "strings::TermRegistry::EagerProofGenerator")
+              : nullptr)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_zero = nm->mkConst(Rational(0));
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index 7d660e019..ba973fac8 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -22,6 +22,7 @@
 #include "context/cdlist.h"
 #include "proof/eager_proof_generator.h"
 #include "proof/proof_node_manager.h"
+#include "smt/env_obj.h"
 #include "theory/output_channel.h"
 #include "theory/strings/infer_info.h"
 #include "theory/strings/sequences_stats.h"
@@ -44,14 +45,15 @@ class InferenceManager;
  * (5) Maintaining a skolem cache. Notice that this skolem cache is the
  * official skolem cache that should be used by all modules in TheoryStrings.
  */
-class TermRegistry
+class TermRegistry : protected EnvObj
 {
   typedef context::CDHashSet<Node> NodeSet;
   typedef context::CDHashSet<TypeNode, std::hash<TypeNode>> TypeNodeSet;
   typedef context::CDHashMap<Node, Node> NodeNodeMap;
 
  public:
-  TermRegistry(SolverState& s,
+  TermRegistry(Env& env,
+               SolverState& s,
                SequencesStatistics& statistics,
                ProofNodeManager* pnm);
   ~TermRegistry();
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3e807c3ac..1b315447e 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -56,14 +56,15 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
       d_statistics(),
       d_state(env, d_valuation),
       d_eagerSolver(d_state),
-      d_termReg(d_state, d_statistics, d_pnm),
+      d_termReg(env, d_state, d_statistics, d_pnm),
       d_extTheoryCb(),
       d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm),
       d_extTheory(d_extTheoryCb, context(), userContext(), d_im),
       d_rewriter(&d_statistics.d_rewrites),
-      d_bsolver(d_state, d_im),
-      d_csolver(d_state, d_im, d_termReg, d_bsolver),
-      d_esolver(d_state,
+      d_bsolver(env, d_state, d_im),
+      d_csolver(env, d_state, d_im, d_termReg, d_bsolver),
+      d_esolver(env,
+                d_state,
                 d_im,
                 d_termReg,
                 d_rewriter,
@@ -71,14 +72,15 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
                 d_csolver,
                 d_extTheory,
                 d_statistics),
-      d_rsolver(d_state,
+      d_rsolver(env,
+                d_state,
                 d_im,
                 d_termReg.getSkolemCache(),
                 d_csolver,
                 d_esolver,
                 d_statistics),
       d_regexp_elim(options::regExpElimAgg(), d_pnm, userContext()),
-      d_stringsFmf(context(), userContext(), valuation, d_termReg)
+      d_stringsFmf(env, valuation, d_termReg)
 {
   d_termReg.finishInit(&d_im);
 
diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index ec7955125..484e27ead 100644
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -27,13 +27,6 @@ TheoryState::TheoryState(Env& env, Valuation val)
 
 void TheoryState::setEqualityEngine(eq::EqualityEngine* ee) { d_ee = ee; }
 
-context::Context* TheoryState::getSatContext() const { return context(); }
-
-context::UserContext* TheoryState::getUserContext() const
-{
-  return userContext();
-}
-
 bool TheoryState::hasTerm(TNode a) const
 {
   Assert(d_ee != nullptr);
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 574aa9355..e8da3ad39 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -42,10 +42,6 @@ class TheoryState : protected EnvObj
    * of theory.
    */
   void setEqualityEngine(eq::EqualityEngine* ee);
-  /** Get the SAT context */
-  context::Context* getSatContext() const;
-  /** Get the user context */
-  context::UserContext* getUserContext() const;
   //-------------------------------------- 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/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 5b919860e..3c71cdbb9 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -186,7 +186,7 @@ void Region::setDisequal( Node n1, Node n2, int type, bool valid ){
 void Region::setRep( Node n, bool valid ) {
   Assert(hasRep(n) != valid);
   if( valid && d_nodes.find( n )==d_nodes.end() ){
-    d_nodes[n] = new RegionNodeInfo(d_cf->d_state.getSatContext());
+    d_nodes[n] = new RegionNodeInfo(d_cf->d_thss->context());
   }
   d_nodes[n]->setValid(valid);
   d_reps_size = d_reps_size + ( valid ? 1 : -1 );
@@ -447,8 +447,8 @@ void Region::debugPrint( const char* c, bool incClique ) {
 }
 
 SortModel::CardinalityDecisionStrategy::CardinalityDecisionStrategy(
-    Node t, context::Context* satContext, Valuation valuation)
-    : DecisionStrategyFmf(satContext, valuation), d_cardinality_term(t)
+    Env& env, Node t, Valuation valuation)
+    : DecisionStrategyFmf(env, valuation), d_cardinality_term(t)
 {
 }
 Node SortModel::CardinalityDecisionStrategy::mkLiteral(unsigned i)
@@ -470,15 +470,15 @@ SortModel::SortModel(Node n,
       d_state(state),
       d_im(im),
       d_thss(thss),
-      d_regions_index(d_state.getSatContext(), 0),
-      d_regions_map(d_state.getSatContext()),
-      d_split_score(d_state.getSatContext()),
-      d_disequalities_index(d_state.getSatContext(), 0),
-      d_reps(d_state.getSatContext(), 0),
-      d_cardinality(d_state.getSatContext(), 1),
-      d_hasCard(d_state.getSatContext(), false),
-      d_maxNegCard(d_state.getSatContext(), 0),
-      d_initialized(d_state.getUserContext(), false),
+      d_regions_index(thss->context(), 0),
+      d_regions_map(thss->context()),
+      d_split_score(thss->context()),
+      d_disequalities_index(thss->context(), 0),
+      d_reps(thss->context(), 0),
+      d_cardinality(thss->context(), 1),
+      d_hasCard(thss->context(), false),
+      d_maxNegCard(thss->context(), 0),
+      d_initialized(thss->userContext(), false),
       d_c_dec_strat(nullptr)
 {
   d_cardinality_term = n;
@@ -489,7 +489,7 @@ SortModel::SortModel(Node n,
     // We are guaranteed that the decision manager is ready since we
     // construct this module during TheoryUF::finishInit.
     d_c_dec_strat.reset(new CardinalityDecisionStrategy(
-        n, d_state.getSatContext(), thss->getTheory()->getValuation()));
+        thss->d_env, n, thss->getTheory()->getValuation()));
   }
 }
 
@@ -530,7 +530,7 @@ void SortModel::newEqClass( Node n ){
         d_regions[d_regions_index]->setValid(true);
         Assert(d_regions[d_regions_index]->getNumReps() == 0);
       }else{
-        d_regions.push_back(new Region(this, d_state.getSatContext()));
+        d_regions.push_back(new Region(this, d_thss->context()));
       }
       d_regions[d_regions_index]->addRep(n);
       d_regions_index = d_regions_index + 1;
@@ -1225,29 +1225,31 @@ Node SortModel::getCardinalityLiteral(uint32_t c)
   return lit;
 }
 
-CardinalityExtension::CardinalityExtension(TheoryState& state,
+CardinalityExtension::CardinalityExtension(Env& env,
+                                           TheoryState& state,
                                            TheoryInferenceManager& im,
                                            TheoryUF* th)
-    : d_state(state),
+    : EnvObj(env),
+      d_state(state),
       d_im(im),
       d_th(th),
       d_rep_model(),
-      d_min_pos_com_card(state.getSatContext(), 0),
-      d_min_pos_com_card_set(state.getSatContext(), false),
+      d_min_pos_com_card(context(), 0),
+      d_min_pos_com_card_set(context(), false),
       d_cc_dec_strat(nullptr),
-      d_initializedCombinedCardinality(state.getUserContext(), false),
-      d_card_assertions_eqv_lemma(state.getUserContext()),
-      d_min_pos_tn_master_card(state.getSatContext(), 0),
-      d_min_pos_tn_master_card_set(state.getSatContext(), false),
-      d_rel_eqc(state.getSatContext())
+      d_initializedCombinedCardinality(userContext(), false),
+      d_card_assertions_eqv_lemma(userContext()),
+      d_min_pos_tn_master_card(context(), 0),
+      d_min_pos_tn_master_card_set(context(), false),
+      d_rel_eqc(context())
 {
   if (options::ufssMode() == options::UfssMode::FULL && options::ufssFairness())
   {
     // Register the strategy with the decision manager of the theory.
     // We are guaranteed that the decision manager is ready since we
     // construct this module during TheoryUF::finishInit.
-    d_cc_dec_strat.reset(new CombinedCardinalityDecisionStrategy(
-        state.getSatContext(), th->getValuation()));
+    d_cc_dec_strat.reset(
+        new CombinedCardinalityDecisionStrategy(env, th->getValuation()));
   }
 }
 
@@ -1560,9 +1562,8 @@ void CardinalityExtension::presolve()
 }
 
 CardinalityExtension::CombinedCardinalityDecisionStrategy::
-    CombinedCardinalityDecisionStrategy(context::Context* satContext,
-                                        Valuation valuation)
-    : DecisionStrategyFmf(satContext, valuation)
+    CombinedCardinalityDecisionStrategy(Env& env, Valuation valuation)
+    : DecisionStrategyFmf(env, valuation)
 {
 }
 Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral(
diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 1809a30bd..10e9ceb44 100644
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -20,6 +20,7 @@
 
 #include "context/cdhashmap.h"
 #include "context/context.h"
+#include "smt/env_obj.h"
 #include "theory/decision_strategy.h"
 #include "theory/theory.h"
 #include "util/statistics_stats.h"
@@ -36,7 +37,7 @@ class TheoryUF;
  * CAV 2013, or Reynolds dissertation "Finite Model Finding in Satisfiability
  * Modulo Theories".
  */
-class CardinalityExtension
+class CardinalityExtension : protected EnvObj
 {
  protected:
   typedef context::CDHashMap<Node, bool> NodeBoolMap;
@@ -340,9 +341,7 @@ class CardinalityExtension
     class CardinalityDecisionStrategy : public DecisionStrategyFmf
     {
      public:
-      CardinalityDecisionStrategy(Node t,
-                                  context::Context* satContext,
-                                  Valuation valuation);
+      CardinalityDecisionStrategy(Env& env, Node t, Valuation valuation);
       /** make literal (the i^th combined cardinality literal) */
       Node mkLiteral(unsigned i) override;
       /** identify */
@@ -357,7 +356,8 @@ class CardinalityExtension
   }; /** class SortModel */
 
  public:
-  CardinalityExtension(TheoryState& state,
+  CardinalityExtension(Env& env,
+                       TheoryState& state,
                        TheoryInferenceManager& im,
                        TheoryUF* th);
   ~CardinalityExtension();
@@ -436,8 +436,7 @@ class CardinalityExtension
   class CombinedCardinalityDecisionStrategy : public DecisionStrategyFmf
   {
    public:
-    CombinedCardinalityDecisionStrategy(context::Context* satContext,
-                                        Valuation valuation);
+    CombinedCardinalityDecisionStrategy(Env& env, Valuation valuation);
     /** make literal (the i^th combined cardinality literal) */
     Node mkLiteral(unsigned i) override;
     /** identify */
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index af2bf4a3b..925805332 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -28,11 +28,14 @@ namespace cvc5 {
 namespace theory {
 namespace uf {
 
-HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im)
-    : d_state(state),
+HoExtension::HoExtension(Env& env,
+                         TheoryState& state,
+                         TheoryInferenceManager& im)
+    : EnvObj(env),
+      d_state(state),
       d_im(im),
-      d_extensionality(state.getUserContext()),
-      d_uf_std_skolem(state.getUserContext())
+      d_extensionality(userContext()),
+      d_uf_std_skolem(userContext())
 {
   d_true = NodeManager::currentNM()->mkConst(true);
 }
diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h
index af8f727fd..a646b57be 100644
--- a/src/theory/uf/ho_extension.h
+++ b/src/theory/uf/ho_extension.h
@@ -22,6 +22,7 @@
 #include "context/cdhashset.h"
 #include "context/cdo.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 #include "theory/theory_inference_manager.h"
 #include "theory/theory_model.h"
 #include "theory/theory_state.h"
@@ -47,13 +48,13 @@ class TheoryUF;
  *
  * For more details, see "Extending SMT Solvers to Higher-Order", Barbosa et al.
  */
-class HoExtension
+class HoExtension : protected EnvObj
 {
   typedef context::CDHashSet<Node> NodeSet;
   typedef context::CDHashMap<Node, Node> NodeNodeMap;
 
  public:
-  HoExtension(TheoryState& state, TheoryInferenceManager& im);
+  HoExtension(Env& env, TheoryState& state, TheoryInferenceManager& im);
 
   /** ppRewrite
    *
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 07820a41d..056b0407a 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -92,7 +92,7 @@ void TheoryUF::finishInit() {
   if (options::finiteModelFind()
       && options::ufssMode() != options::UfssMode::NONE)
   {
-    d_thss.reset(new CardinalityExtension(d_state, d_im, this));
+    d_thss.reset(new CardinalityExtension(d_env, d_state, d_im, this));
   }
   // The kinds we are treating as function application in congruence
   bool isHo = logicInfo().isHigherOrder();
@@ -100,7 +100,7 @@ void TheoryUF::finishInit() {
   if (isHo)
   {
     d_equalityEngine->addFunctionKind(kind::HO_APPLY);
-    d_ho.reset(new HoExtension(d_state, d_im));
+    d_ho.reset(new HoExtension(d_env, d_state, d_im));
   }
 }