From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 24 Feb 2022 05:25:57 +0000 (-0600)
Subject: Make uninterpreted sort owner non-static (#8144)
X-Git-Tag: cvc5-1.0.0~389
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b55ee5396848d20ac502293fc58d2fd915a42f1d;p=cvc5.git

Make uninterpreted sort owner non-static (#8144)

This eliminates the static member `s_uninterpretedSortOwner` from Theory which seems to be the cause of several issues related to the array solver in incremental mode, and with check-unsat-cores. This is moved to a data member of Env.  This eliminates a static access to `theoryOfMode` from within theoryOf calls.

Note that static calls to `Theory::theoryOf` or `Theory::isLeafOf` now assume type-based theoryOf mode as a default argument. Thus, the preferred method for determining theoryOf types and terms is through `Env` now.

This fixes issues with the array solver in incremental mode.

The root issue is that spawning subsolvers (e.g. for check-unsat-core) can overwrite `s_uninterpretedSortOwner`. This means that a second call to `check-sat` (which does not reinitialize set_defaults) will use the *overwrtten* setting, which can be different from what was used for the first check-sat.  In particular, for #5720, the uninterpreted sort owner changes from ARRAYS to UF at the 2nd call, and the array theory solver fails to send an extensionality lemma.

This commit also simplifies `Theory::theoryOf` slightly.

Fixes https://github.com/cvc5/cvc5-wishues/issues/52.
Fixes https://github.com/cvc5/cvc5/issues/5720.
Fixes https://github.com/cvc5/cvc5/issues/6276 .
Fixes https://github.com/cvc5/cvc5/issues/5836.
---

diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index 945f12168..45f09d48e 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -670,7 +670,7 @@ ITESimplifier::~ITESimplifier()
 
 bool ITESimplifier::leavesAreConst(TNode e)
 {
-  return leavesAreConst(e, theory::Theory::theoryOf(e));
+  return leavesAreConst(e, d_env.theoryOf(e));
 }
 
 void ITESimplifier::clearSimpITECaches()
@@ -1258,7 +1258,7 @@ Node ITESimplifier::attemptConstantRemoval(TNode atom)
 bool ITESimplifier::leavesAreConst(TNode e, theory::TheoryId tid)
 {
   Assert((e.getKind() == kind::ITE && !e.getType().isBoolean())
-         || theory::Theory::theoryOf(e) != theory::THEORY_BOOL);
+         || d_env.theoryOf(e) != theory::THEORY_BOOL);
   if (e.isConst())
   {
     return true;
@@ -1539,7 +1539,7 @@ Node ITESimplifier::simpITE(TNode assertion)
     // If node has no ITE's or already in the cache we're done, pop from the
     // stack
     if (current.getNumChildren() == 0
-        || (theory::Theory::theoryOf(current) != theory::THEORY_BOOL
+        || (d_env.theoryOf(current) != theory::THEORY_BOOL
             && !containsTermITE(current)))
     {
       d_simpITECache[current] = current;
@@ -1575,7 +1575,7 @@ Node ITESimplifier::simpITE(TNode assertion)
       Node result = builder;
 
       // If this is an atom, we process it
-      if (theory::Theory::theoryOf(result) != theory::THEORY_BOOL
+      if (d_env.theoryOf(result) != theory::THEORY_BOOL
           && result.getType().isBoolean())
       {
         result = simpITEAtom(result);
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 4026760f7..327649be9 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -35,24 +35,22 @@
 namespace cvc5 {
 namespace prop {
 
-CnfStream::CnfStream(SatSolver* satSolver,
+CnfStream::CnfStream(Env& env,
+                     SatSolver* satSolver,
                      Registrar* registrar,
-                     context::Context* context,
-                     Env* env,
-                     ResourceManager* rm,
+                     context::Context* c,
                      FormulaLitPolicy flpol,
                      std::string name)
-    : d_satSolver(satSolver),
-      d_env(env),
-      d_booleanVariables(context),
-      d_notifyFormulas(context),
-      d_nodeToLiteralMap(context),
-      d_literalToNodeMap(context),
+    : EnvObj(env),
+      d_satSolver(satSolver),
+      d_booleanVariables(c),
+      d_notifyFormulas(c),
+      d_nodeToLiteralMap(c),
+      d_literalToNodeMap(c),
       d_flitPolicy(flpol),
       d_registrar(registrar),
       d_name(name),
       d_removable(false),
-      d_resourceManager(rm),
       d_stats(name)
 {
 }
@@ -128,7 +126,7 @@ void CnfStream::ensureLiteral(TNode n)
   }
   // remove top level negation
   n = n.getKind() == kind::NOT ? n[0] : n;
-  if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
+  if (d_env.theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
   {
     // If we were called with something other than a theory atom (or
     // Boolean variable), we get a SatLiteral that is definitionally
@@ -712,7 +710,7 @@ void CnfStream::convertAndAssert(TNode node, bool negated)
   Trace("cnf") << "convertAndAssert(" << node
                << ", negated = " << (negated ? "true" : "false") << ")\n";
 
-  d_resourceManager->spendResource(Resource::CnfStep);
+  resourceManager()->spendResource(Resource::CnfStep);
 
   switch(node.getKind()) {
     case kind::AND: convertAndAssertAnd(node, negated); break;
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 5a0b5f0b3..d86f27dda 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -33,6 +33,7 @@
 #include "prop/proof_cnf_stream.h"
 #include "prop/registrar.h"
 #include "prop/sat_solver_types.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -64,7 +65,8 @@ enum class FormulaLitPolicy : uint32_t
  * each subexpression in the constructed equi-satisfiable formula, then
  * substitute the new literal for the formula, and so on, recursively.
  */
-class CnfStream {
+class CnfStream : protected EnvObj
+{
   friend PropEngine;
   friend ProofCnfStream;
 
@@ -81,22 +83,19 @@ class CnfStream {
    * and sends the generated clauses and to the given SAT solver. This does not
    * take ownership of satSolver, registrar, or context.
    *
+   * @param env reference to the environment
    * @param satSolver the sat solver to use.
    * @param registrar the entity that takes care of preregistration of Nodes.
-   * @param context the context that the CNF should respect.
-   * @param env Reference to the environment of the smt engine. Assertions
-   * will not be dumped if env == nullptr.
-   * @param rm the resource manager of the CNF stream
+   * @param c the context that the CNF should respect.
    * @param flpol policy for literals corresponding to formulas (those that are
    * not-theory literals).
    * @param name string identifier to distinguish between different instances
    * even for non-theory literals.
    */
-  CnfStream(SatSolver* satSolver,
+  CnfStream(Env& env,
+            SatSolver* satSolver,
             Registrar* registrar,
-            context::Context* context,
-            Env* env,
-            ResourceManager* rm,
+            context::Context* c,
             FormulaLitPolicy flpol = FormulaLitPolicy::INTERNAL,
             std::string name = "");
   /**
@@ -212,9 +211,6 @@ class CnfStream {
   /** The SAT solver we will be using */
   SatSolver* d_satSolver;
 
-  /** Pointer to the env of the smt engine */
-  Env* d_env;
-
   /** Boolean variables that we translated */
   context::CDList<TNode> d_booleanVariables;
 
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index 8aaa68b9a..a3c8d4c71 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -23,14 +23,17 @@
 namespace cvc5 {
 namespace prop {
 
-ProofCnfStream::ProofCnfStream(context::UserContext* u,
+ProofCnfStream::ProofCnfStream(Env& env,
                                CnfStream& cnfStream,
-                               SatProofManager* satPM,
-                               ProofNodeManager* pnm)
-    : d_cnfStream(cnfStream),
+                               SatProofManager* satPM)
+    : EnvObj(env),
+      d_cnfStream(cnfStream),
       d_satPM(satPM),
-      d_proof(pnm, nullptr, u, "ProofCnfStream::LazyCDProof"),
-      d_blocked(u)
+      d_proof(env.getProofNodeManager(),
+              nullptr,
+              userContext(),
+              "ProofCnfStream::LazyCDProof"),
+      d_blocked(userContext())
 {
 }
 
@@ -628,7 +631,7 @@ void ProofCnfStream::ensureLiteral(TNode n)
   // remove top level negation. We don't need to track this because it's a
   // literal.
   n = n.getKind() == kind::NOT ? n[0] : n;
-  if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
+  if (d_env.theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
   {
     // These are not removable
     d_cnfStream.d_removable = false;
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index b79b3098f..1f47203bf 100644
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -27,6 +27,7 @@
 #include "proof/theory_proof_step_buffer.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_proof_manager.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 namespace prop {
@@ -42,13 +43,10 @@ class SatProofManager;
  * that getting the proof of a clausified formula will also extend to its
  * registered proof generator.
  */
-class ProofCnfStream : public ProofGenerator
+class ProofCnfStream : protected EnvObj, public ProofGenerator
 {
  public:
-  ProofCnfStream(context::UserContext* u,
-                 CnfStream& cnfStream,
-                 SatProofManager* satPM,
-                 ProofNodeManager* pnm);
+  ProofCnfStream(Env& env, CnfStream& cnfStream, SatProofManager* satPM);
 
   /** Invokes getProofFor of the underlying LazyCDProof */
   std::shared_ptr<ProofNode> getProofFor(Node f) override;
@@ -166,8 +164,6 @@ class ProofCnfStream : public ProofGenerator
   CnfStream& d_cnfStream;
   /** The proof manager of underlying SAT solver associated with this stream. */
   SatProofManager* d_satPM;
-  /** The proof node manager. */
-  ProofNodeManager* d_pnm;
   /** The user-context-dependent proof object. */
   LazyCDProof d_proof;
   /** An accumulator of steps that may be applied to normalize the clauses
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index b2b432723..c14b0183d 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -81,7 +81,6 @@ PropEngine::PropEngine(Env& env, TheoryEngine* te)
   Debug("prop") << "Constructing the PropEngine" << std::endl;
   context::UserContext* userContext = d_env.getUserContext();
   ProofNodeManager* pnm = d_env.getProofNodeManager();
-  ResourceManager* rm = d_env.getResourceManager();
 
   options::DecisionMode dmode = options().decision.decisionMode;
   if (dmode == options::DecisionMode::JUSTIFICATION
@@ -106,11 +105,10 @@ PropEngine::PropEngine(Env& env, TheoryEngine* te)
   // theory proxy first
   d_theoryProxy = new TheoryProxy(
       d_env, this, d_theoryEngine, d_decisionEngine.get(), d_skdm.get());
-  d_cnfStream = new CnfStream(d_satSolver,
+  d_cnfStream = new CnfStream(env,
+                              d_satSolver,
                               d_theoryProxy,
                               userContext,
-                              &d_env,
-                              rm,
                               FormulaLitPolicy::TRACK,
                               "prop");
 
@@ -127,10 +125,9 @@ PropEngine::PropEngine(Env& env, TheoryEngine* te)
   if (satProofs)
   {
     d_pfCnfStream.reset(new ProofCnfStream(
-        userContext,
+        env,
         *d_cnfStream,
-        static_cast<MinisatSatSolver*>(d_satSolver)->getProofManager(),
-        pnm));
+        static_cast<MinisatSatSolver*>(d_satSolver)->getProofManager()));
     d_ppm.reset(
         new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get()));
   }
@@ -383,7 +380,7 @@ Result PropEngine::checkSat() {
   }
 
   if( result == SAT_VALUE_UNKNOWN ) {
-    ResourceManager* rm = d_env.getResourceManager();
+    ResourceManager* rm = resourceManager();
     Result::UnknownExplanation why = Result::INTERRUPTED;
     if (rm->outOfTime())
     {
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 41bf8a482..29c232011 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -27,6 +27,7 @@
 #include "smt/solver_engine_stats.h"
 #include "theory/evaluator.h"
 #include "theory/rewriter.h"
+#include "theory/theory.h"
 #include "theory/trust_substitutions.h"
 #include "util/resource_manager.h"
 #include "util/statistics_registry.h"
@@ -48,7 +49,8 @@ Env::Env(NodeManager* nm, const Options* opts)
       d_statisticsRegistry(std::make_unique<StatisticsRegistry>(*this)),
       d_options(),
       d_originalOptions(opts),
-      d_resourceManager()
+      d_resourceManager(),
+      d_uninterpretedSortOwner(theory::THEORY_UF)
 {
   if (opts != nullptr)
   {
@@ -233,4 +235,25 @@ bool Env::isFiniteType(TypeNode tn) const
                                   d_options.quantifiers.finiteModelFind);
 }
 
+void Env::setUninterpretedSortOwner(theory::TheoryId theory)
+{
+  d_uninterpretedSortOwner = theory;
+}
+
+theory::TheoryId Env::getUninterpretedSortOwner() const
+{
+  return d_uninterpretedSortOwner;
+}
+
+theory::TheoryId Env::theoryOf(TypeNode typeNode) const
+{
+  return theory::Theory::theoryOf(typeNode, d_uninterpretedSortOwner);
+}
+
+theory::TheoryId Env::theoryOf(TNode node) const
+{
+  return theory::Theory::theoryOf(
+      node, d_options.theory.theoryOfMode, d_uninterpretedSortOwner);
+}
+
 }  // namespace cvc5
diff --git a/src/smt/env.h b/src/smt/env.h
index fd90386d7..391c0b6f3 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -24,6 +24,7 @@
 #include "options/options.h"
 #include "proof/method_id.h"
 #include "theory/logic_info.h"
+#include "theory/theory_id.h"
 #include "util/statistics_registry.h"
 
 namespace cvc5 {
@@ -235,6 +236,26 @@ class Env
    */
   bool isFiniteType(TypeNode tn) const;
 
+  /**
+   * Set the owner of the uninterpreted sort.
+   */
+  void setUninterpretedSortOwner(theory::TheoryId theory);
+
+  /**
+   * Get the owner of the uninterpreted sort.
+   */
+  theory::TheoryId getUninterpretedSortOwner() const;
+
+  /**
+   * Return the ID of the theory responsible for the given type.
+   */
+  theory::TheoryId theoryOf(TypeNode typeNode) const;
+
+  /**
+   * Returns the ID of the theory responsible for the given node.
+   */
+  theory::TheoryId theoryOf(TNode node) const;
+
  private:
   /* Private initialization ------------------------------------------------- */
 
@@ -308,6 +329,8 @@ class Env
   const Options* d_originalOptions;
   /** Manager for limiting time and abstract resource usage. */
   std::unique_ptr<ResourceManager> d_resourceManager;
+  /** The theory that owns the uninterpreted sort. */
+  theory::TheoryId d_uninterpretedSortOwner;
 }; /* class Env */
 
 }  // namespace cvc5
diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index dd0cd3610..f8affe42b 100644
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -89,7 +89,7 @@ TrustNode ExpandDefs::expandDefinitions(TNode n,
         result.push(ret.isNull() ? n : ret);
         continue;
       }
-      theory::TheoryId tid = theory::Theory::theoryOf(node);
+      theory::TheoryId tid = d_env.theoryOf(node);
       theory::TheoryRewriter* tr = rr->getTheoryRewriter(tid);
 
       Assert(tr != NULL);
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 167a82e26..07f5e2c35 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -976,7 +976,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
   {
     // get the kind of rewrite
     MethodId idr = MethodId::RW_REWRITE;
-    TheoryId theoryId = Theory::theoryOf(args[0]);
+    TheoryId theoryId = d_env.theoryOf(args[0]);
     if (args.size() >= 2)
     {
       getMethodId(args[1], idr);
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index e444ea275..c3008f2dd 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -515,11 +515,11 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
       && (!logic.isQuantified()
           || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF))))
   {
-    Theory::setUninterpretedSortOwner(THEORY_ARRAYS);
+    d_env.setUninterpretedSortOwner(THEORY_ARRAYS);
   }
   else
   {
-    Theory::setUninterpretedSortOwner(THEORY_UF);
+    d_env.setUninterpretedSortOwner(THEORY_UF);
   }
 
   if (!opts.smt.simplifyWithCareEnabledWasSetByUser)
diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp
index 6d9a71722..4aa9f009e 100644
--- a/src/theory/arith/branch_and_bound.cpp
+++ b/src/theory/arith/branch_and_bound.cpp
@@ -66,7 +66,7 @@ TrustNode BranchAndBound::branchIntegerVariable(TNode var, Rational value)
     // Also preprocess it before we send it out. This is important since
     // arithmetic may prefer eliminating equalities.
     TrustNode teq;
-    if (Theory::theoryOf(eq) == THEORY_ARITH)
+    if (d_env.theoryOf(eq) == THEORY_ARITH)
     {
       teq = d_ppre.ppRewriteEq(eq);
       eq = teq.isNull() ? eq : teq.getNode();
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 5218baf9b..4480fdbb3 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -133,7 +133,7 @@ TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
   {
     return d_ppre.ppRewriteEq(atom);
   }
-  Assert(Theory::theoryOf(atom) == THEORY_ARITH);
+  Assert(d_env.theoryOf(atom) == THEORY_ARITH);
   // Eliminate operators. Notice we must do this here since other
   // theories may generate lemmas that involve non-standard operators. For
   // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index d0c5125f7..b3667fa86 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -342,11 +342,10 @@ void BVSolverBitblast::initSatSolver()
           d_env.getResourceManager(),
           "theory::bv::BVSolverBitblast::"));
   }
-  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
+  d_cnfStream.reset(new prop::CnfStream(d_env,
+                                        d_satSolver.get(),
                                         d_bbRegistrar.get(),
                                         d_nullContext.get(),
-                                        nullptr,
-                                        d_env.getResourceManager(),
                                         prop::FormulaLitPolicy::INTERNAL,
                                         "theory::bv::BVSolverBitblast"));
 }
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 2a040f75c..df57aa556 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -161,7 +161,7 @@ static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
       continue;
     }
 
-    if (theory::Theory::theoryOf(options::TheoryOfMode::THEORY_OF_TERM_BASED, n)
+    if (theory::Theory::theoryOf(n, options::TheoryOfMode::THEORY_OF_TERM_BASED)
         == theory::THEORY_BV)
     {
       Kind k = n.getKind();
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 461e9f4cc..046bb9de8 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -869,7 +869,7 @@ EvalResult Evaluator::evalInternal(
 
             default:
             {
-              Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0])
+              Trace("evaluator") << "Evaluation of " << currNode[0].getKind()
                                  << " not supported" << std::endl;
               results[currNode] = EvalResult();
               evalAsNode[currNode] =
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 051d457ea..414ff2e3b 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -521,7 +521,7 @@ void CegInstantiator::registerTheoryIds(TypeNode tn,
   if (visited.find(tn) == visited.end())
   {
     visited[tn] = true;
-    TheoryId tid = Theory::theoryOf(tn);
+    TheoryId tid = d_env.theoryOf(tn);
     registerTheoryId(tid);
     if (tn.isDatatype())
     {
@@ -861,7 +861,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
   std::unordered_set<Node> lits;
   for (unsigned r = 0; r < 2; r++)
   {
-    TheoryId tid = r == 0 ? Theory::theoryOf(pvtn) : THEORY_UF;
+    TheoryId tid = r == 0 ? d_env.theoryOf(pvtn) : THEORY_UF;
     Trace("cegqi-inst-debug2") << "  look at assertions of " << tid << std::endl;
     std::map<TheoryId, std::vector<Node> >::iterator ita =
         d_curr_asserts.find(tid);
@@ -1399,7 +1399,7 @@ void CegInstantiator::processAssertions() {
   while( !eqcs_i.isFinished() ){
     Node r = *eqcs_i;
     TypeNode rtn = r.getType();
-    TheoryId tid = Theory::theoryOf( rtn );
+    TheoryId tid = d_env.theoryOf(rtn);
     //if we care about the theory of this eqc
     if( std::find( d_tids.begin(), d_tids.end(), tid )!=d_tids.end() ){
       if (rtn.isRealOrInt())
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 27e75fd83..bcc22b646 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -46,7 +46,7 @@ bool isAlreadyVisited(Env& env,
                       TNode current,
                       TNode parent)
 {
-  TheoryId currentTheoryId = Theory::theoryOf(current);
+  TheoryId currentTheoryId = env.theoryOf(current);
   if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
   {
     // current theory not visited, return false
@@ -61,7 +61,7 @@ bool isAlreadyVisited(Env& env,
 
   // The current theory has already visited it, so now it depends on the parent
   // and the type
-  TheoryId parentTheoryId = Theory::theoryOf(parent);
+  TheoryId parentTheoryId = env.theoryOf(parent);
   if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
   {
     // parent theory not visited, return false
@@ -75,7 +75,7 @@ bool isAlreadyVisited(Env& env,
     // current and parent are the same theory, and we are infinite, return true
     return true;
   }
-  TheoryId typeTheoryId = Theory::theoryOf(type);
+  TheoryId typeTheoryId = env.theoryOf(type);
   return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
 }
 
@@ -144,14 +144,14 @@ void PreRegisterVisitor::preRegister(Env& env,
                                      TheoryIdSet preregTheories)
 {
   // Preregister with the current theory, if necessary
-  TheoryId currentTheoryId = Theory::theoryOf(current);
+  TheoryId currentTheoryId = env.theoryOf(current);
   preRegisterWithTheory(
       te, visitedTheories, currentTheoryId, current, parent, preregTheories);
 
   if (current != parent)
   {
     // preregister with parent theory, if necessary
-    TheoryId parentTheoryId = Theory::theoryOf(parent);
+    TheoryId parentTheoryId = env.theoryOf(parent);
     preRegisterWithTheory(
         te, visitedTheories, parentTheoryId, current, parent, preregTheories);
 
@@ -161,7 +161,7 @@ void PreRegisterVisitor::preRegister(Env& env,
     if (currentTheoryId != parentTheoryId || env.isFiniteType(type))
     {
       // preregister with the type's theory, if necessary
-      TheoryId typeTheoryId = Theory::theoryOf(type);
+      TheoryId typeTheoryId = env.theoryOf(type);
       preRegisterWithTheory(
           te, visitedTheories, typeTheoryId, current, parent, preregTheories);
     }
@@ -280,7 +280,7 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
       TheoryIdSetUtil::setUnion(preregTheories, visitedTheories);
 
   // If there is more than two theories and a new one has been added notify the shared terms database
-  TheoryId currentTheoryId = Theory::theoryOf(current);
+  TheoryId currentTheoryId = d_env.theoryOf(current);
   if (TheoryIdSetUtil::setDifference(
           visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
   {
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index f826209b4..54bdebbba 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -42,9 +42,6 @@ using namespace std;
 namespace cvc5 {
 namespace theory {
 
-/** Default value for the uninterpreted sorts is the UF theory */
-TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
-
 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
   switch(level){
   case Theory::EFFORT_STANDARD:
@@ -144,7 +141,9 @@ void Theory::finishInitStandalone()
   finishInit();
 }
 
-TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
+TheoryId Theory::theoryOf(TNode node,
+                          options::TheoryOfMode mode,
+                          TheoryId usortOwner)
 {
   TheoryId tid = THEORY_BUILTIN;
   switch(mode) {
@@ -158,13 +157,13 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
         }
         else
         {
-          tid = Theory::theoryOf(node.getType());
+          tid = theoryOf(node.getType(), usortOwner);
         }
       }
       else if (node.getKind() == kind::EQUAL)
       {
         // Equality is owned by the theory that owns the domain
-        tid = Theory::theoryOf(node[0].getType());
+        tid = theoryOf(node[0].getType(), usortOwner);
       }
       else
       {
@@ -178,10 +177,10 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
       // Variables
       if (node.isVar())
       {
-        if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
+        if (theoryOf(node.getType(), usortOwner) != theory::THEORY_BOOL)
         {
           // We treat the variables as uninterpreted
-          tid = s_uninterpretedSortOwner;
+          tid = THEORY_UF;
         }
         else
         {
@@ -199,60 +198,47 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
       }
       else if (node.getKind() == kind::EQUAL)
       {  // Equality
-        // If one of them is an ITE, it's irelevant, since they will get
-        // replaced out anyhow
-        if (node[0].getKind() == kind::ITE)
-        {
-          tid = Theory::theoryOf(node[0].getType());
-        }
-        else if (node[1].getKind() == kind::ITE)
+        TNode l = node[0];
+        TNode r = node[1];
+        TypeNode ltype = l.getType();
+        TypeNode rtype = r.getType();
+        // If the types are different, we must assign based on type due
+        // to handling subtypes (limited to arithmetic). Also, if we are
+        // a Boolean equality, we must assign THEORY_BOOL.
+        if (ltype != rtype || ltype.isBoolean())
         {
-          tid = Theory::theoryOf(node[1].getType());
+          tid = theoryOf(ltype, usortOwner);
         }
         else
         {
-          TNode l = node[0];
-          TNode r = node[1];
-          TypeNode ltype = l.getType();
-          TypeNode rtype = r.getType();
-          // If the types are different, we must assign based on type due
-          // to handling subtypes (limited to arithmetic). Also, if we are
-          // a Boolean equality, we must assign THEORY_BOOL.
-          if (ltype != rtype || ltype.isBoolean())
+          // If both sides belong to the same theory the choice is easy
+          TheoryId T1 = theoryOf(l, mode, usortOwner);
+          TheoryId T2 = theoryOf(r, mode, usortOwner);
+          if (T1 == T2)
           {
-            tid = Theory::theoryOf(ltype);
+            tid = T1;
           }
           else
           {
-            // If both sides belong to the same theory the choice is easy
-            TheoryId T1 = Theory::theoryOf(l);
-            TheoryId T2 = Theory::theoryOf(r);
-            if (T1 == T2)
+            TheoryId T3 = theoryOf(ltype, usortOwner);
+            // This is a case of
+            // * x*y = f(z) -> UF
+            // * x = c      -> UF
+            // * f(x) = read(a, y) -> either UF or ARRAY
+            // at least one of the theories has to be parametric, i.e. theory
+            // of the type is different from the theory of the term
+            if (T1 == T3)
+            {
+              tid = T2;
+            }
+            else if (T2 == T3)
             {
               tid = T1;
             }
             else
             {
-              TheoryId T3 = Theory::theoryOf(ltype);
-              // This is a case of
-              // * x*y = f(z) -> UF
-              // * x = c      -> UF
-              // * f(x) = read(a, y) -> either UF or ARRAY
-              // at least one of the theories has to be parametric, i.e. theory
-              // of the type is different from the theory of the term
-              if (T1 == T3)
-              {
-                tid = T2;
-              }
-              else if (T2 == T3)
-              {
-                tid = T1;
-              }
-              else
-              {
-                // If both are parametric, we take the smaller one (arbitrary)
-                tid = T1 < T2 ? T1 : T2;
-              }
+              // If both are parametric, we take the smaller one (arbitrary)
+              tid = T1 < T2 ? T1 : T2;
             }
           }
         }
@@ -267,7 +253,6 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
   default:
     Unreachable();
   }
-  Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
   return tid;
 }
 
@@ -439,7 +424,7 @@ void Theory::collectTerms(TNode n, std::set<Node>& termSet) const
       termSet.insert(cur);
     }
     // traverse owned terms, don't go under quantifiers
-    if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == d_id)
+    if ((k == kind::NOT || k == kind::EQUAL || d_env.theoryOf(cur) == d_id)
         && !cur.isClosure())
     {
       visit.insert(visit.end(), cur.begin(), cur.end());
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 5ef6b337d..f0d147d07 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -196,11 +196,6 @@ class Theory : protected EnvObj
    */
   virtual void declareSepHeap(TypeNode locT, TypeNode dataT) {}
 
-  /**
-   * The theory that owns the uninterpreted sort.
-   */
-  static TheoryId s_uninterpretedSortOwner;
-
   void printFacts(std::ostream& os) const;
   void debugPrintFacts() const;
 
@@ -294,9 +289,9 @@ class Theory : protected EnvObj
   /**
    * Return the ID of the theory responsible for the given type.
    */
-  static inline TheoryId theoryOf(TypeNode typeNode)
+  static inline TheoryId theoryOf(TypeNode typeNode,
+                                  TheoryId usortOwner = theory::THEORY_UF)
   {
-    Trace("theory::internal") << "theoryOf(" << typeNode << ")" << std::endl;
     TheoryId id;
     if (typeNode.getKind() == kind::TYPE_CONSTANT)
     {
@@ -308,10 +303,7 @@ class Theory : protected EnvObj
     }
     if (id == THEORY_BUILTIN)
     {
-      Trace("theory::internal")
-          << "theoryOf(" << typeNode << ") == " << s_uninterpretedSortOwner
-          << std::endl;
-      return s_uninterpretedSortOwner;
+      return usortOwner;
     }
     return id;
   }
@@ -319,46 +311,29 @@ class Theory : protected EnvObj
   /**
    * Returns the ID of the theory responsible for the given node.
    */
-  static TheoryId theoryOf(options::TheoryOfMode mode, TNode node);
-
-  /**
-   * Returns the ID of the theory responsible for the given node.
-   */
-  static inline TheoryId theoryOf(TNode node)
-  {
-    return theoryOf(options::theoryOfMode(), node);
-  }
-
-  /**
-   * Set the owner of the uninterpreted sort.
-   */
-  static void setUninterpretedSortOwner(TheoryId theory)
-  {
-    s_uninterpretedSortOwner = theory;
-  }
-
-  /**
-   * Get the owner of the uninterpreted sort.
-   */
-  static TheoryId getUninterpretedSortOwner()
-  {
-    return s_uninterpretedSortOwner;
-  }
+  static TheoryId theoryOf(
+      TNode node,
+      options::TheoryOfMode mode = options::TheoryOfMode::THEORY_OF_TYPE_BASED,
+      TheoryId usortOwner = theory::THEORY_UF);
 
   /**
-   * Checks if the node is a leaf node of this theory
+   * Checks if the node is a leaf node of this theory.
    */
   inline bool isLeaf(TNode node) const
   {
-    return node.getNumChildren() == 0 || theoryOf(node) != d_id;
+    return node.getNumChildren() == 0
+           || theoryOf(node, options().theory.theoryOfMode) != d_id;
   }
 
   /**
    * Checks if the node is a leaf node of a theory.
    */
-  inline static bool isLeafOf(TNode node, TheoryId theoryId)
+  inline static bool isLeafOf(
+      TNode node,
+      TheoryId theoryId,
+      options::TheoryOfMode mode = options::TheoryOfMode::THEORY_OF_TYPE_BASED)
   {
-    return node.getNumChildren() == 0 || theoryOf(node) != theoryId;
+    return node.getNumChildren() == 0 || theoryOf(node, mode) != theoryId;
   }
 
   /** Returns true if the assertFact queue is empty*/
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 173a93566..067dc8b0c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -725,11 +725,12 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
 
-  if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) &&
-     Theory::theoryOf(atom) != THEORY_SAT_SOLVER) {
+  theory::TheoryId tid = d_env.theoryOf(atom);
+  if (!d_logicInfo.isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
+  {
     stringstream ss;
     ss << "The logic was specified as " << d_logicInfo.getLogicString()
-       << ", which doesn't include " << Theory::theoryOf(atom)
+       << ", which doesn't include " << tid
        << ", but got a preprocessing-time fact for that theory." << endl
        << "The fact:" << endl
        << literal;
@@ -865,7 +866,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
             assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
     {
       // Is it preregistered
-      bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
+      bool preregistered = d_propEngine->isSatLiteral(assertion)
+                           && d_env.theoryOf(assertion) == toTheoryId;
       // We assert it
       theoryOf(toTheoryId)->assertFact(assertion, preregistered);
       // Mark that we have more information
@@ -928,7 +930,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
           assertion, originalAssertion, toTheoryIdProp, fromTheoryId))
   {
     // Check if has been pre-registered with the theory
-    bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
+    bool preregistered = d_propEngine->isSatLiteral(assertion)
+                         && d_env.theoryOf(assertion) == toTheoryId;
     // Assert away
     theoryOf(toTheoryId)->assertFact(assertion, preregistered);
     d_factsAsserted = true;
@@ -961,7 +964,10 @@ void TheoryEngine::assertFact(TNode literal)
     // to the assert the equality to the interested theories
     if (atom.getKind() == kind::EQUAL) {
       // Assert it to the the owning theory
-      assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
+      assertToTheory(literal,
+                     literal,
+                     /* to */ d_env.theoryOf(atom),
+                     /* from */ THEORY_SAT_SOLVER);
       // Shared terms manager will assert to interested theories directly, as
       // the terms become shared
       assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
@@ -981,11 +987,17 @@ void TheoryEngine::assertFact(TNode literal)
 
     } else {
       // Not an equality, just assert to the appropriate theory
-      assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
+      assertToTheory(literal,
+                     literal,
+                     /* to */ d_env.theoryOf(atom),
+                     /* from */ THEORY_SAT_SOLVER);
     }
   } else {
     // Assert the fact to the appropriate theory directly
-    assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
+    assertToTheory(literal,
+                   literal,
+                   /* to */ d_env.theoryOf(atom),
+                   /* from */ THEORY_SAT_SOLVER);
   }
 }
 
@@ -1094,7 +1106,7 @@ Node TheoryEngine::getModelValue(TNode var) {
   }
   Assert(d_sharedSolver->isShared(var))
       << "node " << var << " is not shared" << std::endl;
-  return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
+  return theoryOf(d_env.theoryOf(var.getType()))->getModelValue(var);
 }
 
 TrustNode TheoryEngine::getExplanation(TNode node)
@@ -1257,7 +1269,8 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
 
     // If the theory is asking about a different form, or the form is ok but if will go to a different theory
     // then we must figure it out
-    if (eqNormalized != eq || Theory::theoryOf(eq) != atomsTo) {
+    if (eqNormalized != eq || d_env.theoryOf(eq) != atomsTo)
+    {
       // If you get eqNormalized, send atoms[i] to atomsTo
       d_atomRequests.add(eqNormalized, eq, atomsTo);
     }
@@ -1911,7 +1924,7 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
     return std::pair<bool, Node>(false, Node::null());
   }else{
     //it is a theory atom
-    theory::TheoryId tid = theory::Theory::theoryOf(mode, atom);
+    theory::TheoryId tid = Theory::theoryOf(atom, mode);
     theory::Theory* th = theoryOf(tid);
 
     Assert(th != NULL);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index f8a8fd736..c107ef1a9 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -313,7 +313,7 @@ class TheoryEngine : protected EnvObj
    */
   theory::Theory* theoryOf(TNode node) const
   {
-    return d_theoryTable[theory::Theory::theoryOf(node)];
+    return d_theoryTable[d_env.theoryOf(node)];
   }
 
   /**
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6a0ec1f73..b89f1da47 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -119,6 +119,11 @@ set(regress_0_tests
   regress0/arrays/issue4780-3.smt2
   regress0/arrays/issue4780.smt2
   regress0/arrays/issue4927-unsat-cores.smt2
+  regress0/arrays/issue5720.smt2
+  regress0/arrays/issue5836-2.smt2
+  regress0/arrays/issue5836.smt2
+  regress0/arrays/issue6276-2.smt2
+  regress0/arrays/issue6276.smt2
   regress0/arrays/issue6807-idem-rew.smt2
   regress0/arrays/issue7596-define-array-uminus.smt2
   regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
diff --git a/test/regress/regress0/arrays/issue5720.smt2 b/test/regress/regress0/arrays/issue5720.smt2
new file mode 100644
index 000000000..8d0f81f80
--- /dev/null
+++ b/test/regress/regress0/arrays/issue5720.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: -i
+; EXPECT: unsat
+; EXPECT: sat
+(set-logic QF_ALIA)
+(set-option :check-unsat-cores true)
+(set-option :fmf-fun true)
+(declare-fun arr0 () (Array Bool Int))
+(declare-fun arr1 () (Array Int (Array Bool Int)))
+(assert (xor true (= arr1 (store arr1 0 arr0))))
+(push)
+(assert false)
+(check-sat)
+(pop)
+(check-sat)
diff --git a/test/regress/regress0/arrays/issue5836-2.smt2 b/test/regress/regress0/arrays/issue5836-2.smt2
new file mode 100644
index 000000000..43b7d54b9
--- /dev/null
+++ b/test/regress/regress0/arrays/issue5836-2.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic QF_UFNRA)
+(set-info :status sat)
+(declare-fun ufrr5 (Real Real Real Real Real) Real)
+(declare-fun r5 () Real)
+(declare-fun r6 () Real)
+(declare-fun r37 () Real)
+(declare-fun r58 () Real)
+(assert (and (> 0.0 r37) (> r37 (ufrr5 0.0 1.0 1.0 r5 1.0)) (= 0.0 (+ (- 1) (* r6 r58 (- 1))))))
+(assert (= 0.0 (/ 1.0 r5)))
+(check-sat)
diff --git a/test/regress/regress0/arrays/issue5836.smt2 b/test/regress/regress0/arrays/issue5836.smt2
new file mode 100644
index 000000000..2ded5fbd6
--- /dev/null
+++ b/test/regress/regress0/arrays/issue5836.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFLRA)
+(set-info :status sat)
+(declare-fun f (Bool Bool Bool Bool Bool) Bool)
+(declare-fun v () Bool)
+(declare-fun r () Real)
+(declare-fun r5 () Real)
+(declare-fun -6 () (Array Real Real))
+(declare-fun -9 () (Array Bool (Array Real Real)))
+(assert (f true v true false false))
+(assert (= (store -9 true -6) (store -9 false (store -6 r5 0))))
+(assert (distinct r r5 (select -6 r)))
+(check-sat)
diff --git a/test/regress/regress0/arrays/issue6276-2.smt2 b/test/regress/regress0/arrays/issue6276-2.smt2
new file mode 100644
index 000000000..98b9404a2
--- /dev/null
+++ b/test/regress/regress0/arrays/issue6276-2.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic QF_ALIA)
+(set-info :status sat)
+(declare-fun i2 () Int)
+(declare-fun arr0 () (Array Int Bool))
+(declare-fun i10 () Int)
+(assert (select (store (store arr0 1 true) i10 false) i2))
+(push)
+(assert (= i10 0))
+(check-sat)
diff --git a/test/regress/regress0/arrays/issue6276.smt2 b/test/regress/regress0/arrays/issue6276.smt2
new file mode 100644
index 000000000..1cb3b6d9c
--- /dev/null
+++ b/test/regress/regress0/arrays/issue6276.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_ALIA)
+(declare-fun v0 () Bool)
+(declare-fun i1 () Int)
+(declare-fun arr0 () (Array Int Bool))
+(assert (select (store arr0 0 v0) i1))
+(push)
+(assert (= 1 i1))
+(check-sat)
+(check-sat)
diff --git a/test/regress/regress0/bug421.smt2 b/test/regress/regress0/bug421.smt2
index f011638fb..aa2e70122 100644
--- a/test/regress/regress0/bug421.smt2
+++ b/test/regress/regress0/bug421.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --incremental --abstract-values
 ; EXPECT: sat
-; EXPECT: ((a (as @a_2 (Array Int Int))) (b (as @a_3 (Array Int Int))))
+; EXPECT: ((a (as @a_1 (Array Int Int))) (b (as @a_2 (Array Int Int))))
 (set-logic QF_AUFLIA)
 (set-option :produce-models true)
 (declare-fun a () (Array Int Int))
diff --git a/test/regress/regress0/bug421b.smt2 b/test/regress/regress0/bug421b.smt2
index e8d214fad..72942a24e 100644
--- a/test/regress/regress0/bug421b.smt2
+++ b/test/regress/regress0/bug421b.smt2
@@ -4,7 +4,7 @@
 ;
 ; COMMAND-LINE: --incremental --abstract-values --check-models
 ; EXPECT: sat
-; EXPECT: ((a (as @a_2 (Array Int Int))) (b (as @a_3 (Array Int Int))))
+; EXPECT: ((a (as @a_1 (Array Int Int))) (b (as @a_2 (Array Int Int))))
 (set-logic QF_AUFLIA)
 (set-option :produce-models true)
 (declare-fun a () (Array Int Int))
diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp
index 354d57a4e..d29ef69cc 100644
--- a/test/unit/prop/cnf_stream_white.cpp
+++ b/test/unit/prop/cnf_stream_white.cpp
@@ -112,11 +112,10 @@ class TestPropWhiteCnfStream : public TestSmt
     d_cnfContext.reset(new context::Context());
     d_cnfRegistrar.reset(new prop::NullRegistrar);
     d_cnfStream.reset(
-        new cvc5::prop::CnfStream(d_satSolver.get(),
+        new cvc5::prop::CnfStream(d_slvEngine->getEnv(),
+                                  d_satSolver.get(),
                                   d_cnfRegistrar.get(),
-                                  d_cnfContext.get(),
-                                  &d_slvEngine->getEnv(),
-                                  d_slvEngine->getResourceManager()));
+                                  d_cnfContext.get()));
   }
 
   void TearDown() override