Eliminate currentSmtEngine for subsolver calls (#7068)

This eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls.

43 files changed, 212 insertions, 118 deletions

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 33a2e38d9..c0cddda5e 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -295,7 +295,9 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions,
 
   // make a separate smt call
   std::unique_ptr<SmtEngine> rrSygus;
-  theory::initializeSubsolver(rrSygus);
+  theory::initializeSubsolver(rrSygus,
+                              d_preprocContext->getOptions(),
+                              d_preprocContext->getLogicInfo());
   rrSygus->assertFormula(body);
   Trace("sygus-infer") << "*** Check sat..." << std::endl;
   Result r = rrSygus->checkSat();
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index b21fcb261..7fefafce6 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -36,7 +36,14 @@ PreprocessingPassContext::PreprocessingPassContext(
       d_symsInAssertions(env.getUserContext())
 {
 }
-
+const Options& PreprocessingPassContext::getOptions()
+{
+  return d_env.getOptions();
+}
+const LogicInfo& PreprocessingPassContext::getLogicInfo()
+{
+  return d_env.getLogicInfo();
+}
 theory::TrustSubstitutionMap&
 PreprocessingPassContext::getTopLevelSubstitutions()
 {
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 1af73e453..aab1b453d 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -61,8 +61,10 @@ class PreprocessingPassContext
 
   void spendResource(Resource r);
 
-  /** Get the current logic info of the SmtEngine */
-  const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); }
+  /** Get the options of the environment */
+  const Options& getOptions();
+  /** Get the current logic info of the environment */
+  const LogicInfo& getLogicInfo();
 
   /** Gets a reference to the top-level substitution map */
   theory::TrustSubstitutionMap& getTopLevelSubstitutions();
diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index ff1337fe1..b773d8d57 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -32,7 +32,10 @@ using namespace cvc5::theory;
 namespace cvc5 {
 namespace smt {
 
-AbductionSolver::AbductionSolver(SmtEngine* parent) : d_parent(parent) {}
+AbductionSolver::AbductionSolver(Env& env, SmtEngine* parent)
+    : d_env(env), d_parent(parent)
+{
+}
 
 AbductionSolver::~AbductionSolver() {}
 bool AbductionSolver::getAbduct(const Node& goal,
@@ -48,7 +51,7 @@ bool AbductionSolver::getAbduct(const Node& goal,
   std::vector<Node> axioms = d_parent->getExpandedAssertions();
   std::vector<Node> asserts(axioms.begin(), axioms.end());
   // must expand definitions
-  Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(goal);
+  Node conjn = d_env.getTopLevelSubstitutions().apply(goal);
   // now negate
   conjn = conjn.negate();
   d_abdConj = conjn;
@@ -63,7 +66,7 @@ bool AbductionSolver::getAbduct(const Node& goal,
   Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj
                         << ", solving for " << d_sssf << std::endl;
   // we generate a new smt engine to do the abduction query
-  initializeSubsolver(d_subsolver);
+  initializeSubsolver(d_subsolver, d_env);
   // get the logic
   LogicInfo l = d_subsolver->getLogicInfo().getUnlockedCopy();
   // enable everything needed for sygus
@@ -153,7 +156,7 @@ void AbductionSolver::checkAbduct(Node a)
                           << ": make new SMT engine" << std::endl;
     // Start new SMT engine to check solution
     std::unique_ptr<SmtEngine> abdChecker;
-    initializeSubsolver(abdChecker);
+    initializeSubsolver(abdChecker, d_env);
     Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j
                           << ": asserting formulas" << std::endl;
     for (const Node& e : asserts)
diff --git a/src/smt/abduction_solver.h b/src/smt/abduction_solver.h
index c7f9db035..b408fe060 100644
--- a/src/smt/abduction_solver.h
+++ b/src/smt/abduction_solver.h
@@ -23,6 +23,7 @@
 
 namespace cvc5 {
 
+class Env;
 class SmtEngine;
 
 namespace smt {
@@ -37,7 +38,7 @@ namespace smt {
 class AbductionSolver
 {
  public:
-  AbductionSolver(SmtEngine* parent);
+  AbductionSolver(Env& env, SmtEngine* parent);
   ~AbductionSolver();
   /**
    * This method asks this SMT engine to find an abduct with respect to the
@@ -84,6 +85,8 @@ class AbductionSolver
    * problems.
    */
   bool getAbductInternal(Node& abd);
+  /** Reference to the env */
+  Env& d_env;
   /** The parent SMT engine */
   SmtEngine* d_parent;
   /** The SMT engine subsolver
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index d6677c343..7efefabcd 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -33,7 +33,7 @@ using namespace cvc5::smt;
 
 namespace cvc5 {
 
-Env::Env(NodeManager* nm, Options* opts)
+Env::Env(NodeManager* nm, const Options* opts)
     : d_context(new context::Context()),
       d_userContext(new context::UserContext()),
       d_nodeManager(nm),
diff --git a/src/smt/env.h b/src/smt/env.h
index 68148ec00..7c12c86b9 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -61,7 +61,7 @@ class Env
   /**
    * Construct an Env with the given node manager.
    */
-  Env(NodeManager* nm, Options* opts);
+  Env(NodeManager* nm, const Options* opts);
   /** Destruct the env.  */
   ~Env();
 
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index fbbdb1b90..ab7002205 100644
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -32,7 +32,8 @@ using namespace cvc5::theory;
 namespace cvc5 {
 namespace smt {
 
-InterpolationSolver::InterpolationSolver(SmtEngine* parent) : d_parent(parent)
+InterpolationSolver::InterpolationSolver(Env& env, SmtEngine* parent)
+    : d_env(env), d_parent(parent)
 {
 }
 
@@ -52,10 +53,10 @@ bool InterpolationSolver::getInterpol(const Node& conj,
                           << std::endl;
   std::vector<Node> axioms = d_parent->getExpandedAssertions();
   // must expand definitions
-  Node conjn = d_parent->getEnv().getTopLevelSubstitutions().apply(conj);
+  Node conjn = d_env.getTopLevelSubstitutions().apply(conj);
   std::string name("A");
 
-  quantifiers::SygusInterpol interpolSolver;
+  quantifiers::SygusInterpol interpolSolver(d_env);
   if (interpolSolver.solveInterpolation(
           name, axioms, conjn, grammarType, interpol))
   {
@@ -94,7 +95,7 @@ void InterpolationSolver::checkInterpol(Node interpol,
                             << ": make new SMT engine" << std::endl;
     // Start new SMT engine to check solution
     std::unique_ptr<SmtEngine> itpChecker;
-    initializeSubsolver(itpChecker);
+    initializeSubsolver(itpChecker, d_env);
     Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
                             << ": asserting formulas" << std::endl;
     if (j == 0)
diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h
index 03f8ab6a1..19bb54c61 100644
--- a/src/smt/interpolation_solver.h
+++ b/src/smt/interpolation_solver.h
@@ -23,6 +23,7 @@
 
 namespace cvc5 {
 
+class Env;
 class SmtEngine;
 
 namespace smt {
@@ -37,7 +38,7 @@ namespace smt {
 class InterpolationSolver
 {
  public:
-  InterpolationSolver(SmtEngine* parent);
+  InterpolationSolver(Env& env, SmtEngine* parent);
   ~InterpolationSolver();
 
   /**
@@ -77,6 +78,8 @@ class InterpolationSolver
                      const Node& conj);
 
  private:
+  /** Reference to the env */
+  Env& d_env;
   /** The parent SMT engine */
   SmtEngine* d_parent;
 };
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index fecf65275..67de9728c 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -22,6 +22,7 @@
 #include "options/language.h"
 #include "options/smt_options.h"
 #include "smt/assertions.h"
+#include "smt/env.h"
 #include "smt/smt_engine.h"
 #include "theory/smt_engine_subsolver.h"
 
@@ -147,7 +148,8 @@ std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
   std::unique_ptr<SmtEngine> optChecker;
   // initializeSubSolver will copy the options and theories enabled
   // from the current solver to optChecker and adds timeout
-  theory::initializeSubsolver(optChecker, nullptr, needsTimeout, timeout);
+  theory::initializeSubsolver(
+      optChecker, parentSMTSolver->getEnv(), needsTimeout, timeout);
   // we need to be in incremental mode for multiple objectives since we need to
   // push pop we need to produce models to inrement on our objective
   optChecker->setOption("incremental", "true");
@@ -275,7 +277,10 @@ Result OptimizationSolver::optimizeLexicographicIterative()
 Result OptimizationSolver::optimizeParetoNaiveGIA()
 {
   // initial call to Pareto optimizer, create the checker
-  if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent);
+  if (!d_optChecker)
+  {
+    d_optChecker = createOptCheckerWithTimeout(d_parent);
+  }
   NodeManager* nm = d_optChecker->getNodeManager();
 
   // checks whether the current set of assertions are satisfied or not
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 339ba9ea7..04a960282 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -26,6 +26,7 @@
 
 namespace cvc5 {
 
+class Env;
 class SmtEngine;
 
 namespace smt {
@@ -254,6 +255,8 @@ class OptimizationSolver
  private:
   /**
    * Initialize an SMT subsolver for offline optimization purpose
+   * @param env the environment, which determines options and logic for the
+   * subsolver
    * @param parentSMTSolver the parental solver containing the assertions
    * @param needsTimeout specifies whether it needs timeout for each single
    *    query
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index e675feaa0..087aa0e06 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -32,7 +32,10 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace smt {
 
-QuantElimSolver::QuantElimSolver(SmtSolver& sms) : d_smtSolver(sms) {}
+QuantElimSolver::QuantElimSolver(Env& env, SmtSolver& sms)
+    : d_env(env), d_smtSolver(sms)
+{
+}
 
 QuantElimSolver::~QuantElimSolver() {}
 
@@ -51,7 +54,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
   // ensure the body is rewritten
   q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1]));
   // do nested quantifier elimination if necessary
-  q = quantifiers::NestedQe::doNestedQe(q, true);
+  q = quantifiers::NestedQe::doNestedQe(d_env, q, true);
   Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : "
                   << q << std::endl;
   // tag the quantified formula with the quant-elim attribute
diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h
index 4396694e9..f890deba0 100644
--- a/src/smt/quant_elim_solver.h
+++ b/src/smt/quant_elim_solver.h
@@ -22,6 +22,8 @@
 #include "smt/assertions.h"
 
 namespace cvc5 {
+class Env;
+
 namespace smt {
 
 class SmtSolver;
@@ -37,7 +39,7 @@ class SmtSolver;
 class QuantElimSolver
 {
  public:
-  QuantElimSolver(SmtSolver& sms);
+  QuantElimSolver(Env& env, SmtSolver& sms);
   ~QuantElimSolver();
 
   /**
@@ -95,6 +97,8 @@ class QuantElimSolver
                                 bool isInternalSubsolver);
 
  private:
+  /** Reference to the env */
+  Env& d_env;
   /** The SMT solver, which is used during doQuantifierElimination. */
   SmtSolver& d_smtSolver;
 };
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 45056057d..ea253e4ef 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -84,7 +84,7 @@ using namespace cvc5::theory;
 
 namespace cvc5 {
 
-SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
+SmtEngine::SmtEngine(NodeManager* nm, const Options* optr)
     : d_env(new Env(nm, optr)),
       d_state(new SmtEngineState(*d_env.get(), *this)),
       d_absValues(new AbstractValues(getNodeManager())),
@@ -131,11 +131,9 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // make the SMT solver
   d_smtSolver.reset(new SmtSolver(*d_env.get(), *d_state, *d_pp, *d_stats));
   // make the SyGuS solver
-  d_sygusSolver.reset(
-      new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr));
+  d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver, *d_pp));
   // make the quantifier elimination solver
-  d_quantElimSolver.reset(new QuantElimSolver(*d_smtSolver));
-
+  d_quantElimSolver.reset(new QuantElimSolver(*d_env.get(), *d_smtSolver));
 }
 
 bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); }
@@ -259,12 +257,12 @@ void SmtEngine::finishInit()
   // subsolvers
   if (d_env->getOptions().smt.produceAbducts)
   {
-    d_abductSolver.reset(new AbductionSolver(this));
+    d_abductSolver.reset(new AbductionSolver(*d_env.get(), this));
   }
   if (d_env->getOptions().smt.produceInterpols
       != options::ProduceInterpols::NONE)
   {
-    d_interpolSolver.reset(new InterpolationSolver(this));
+    d_interpolSolver.reset(new InterpolationSolver(*d_env.get(), this));
   }
 
   d_pp->finishInit();
@@ -1119,7 +1117,7 @@ Node SmtEngine::getValue(const Node& ex) const
   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
   if (Dump.isOn("benchmark"))
   {
-    getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex});
+    getPrinter().toStreamCmdGetValue(d_env->getDumpOut(), {ex});
   }
   TypeNode expectedType = ex.getType();
 
@@ -1408,7 +1406,7 @@ std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core)
   for (const Node& skip : core)
   {
     std::unique_ptr<SmtEngine> coreChecker;
-    initializeSubsolver(coreChecker);
+    initializeSubsolver(coreChecker, *d_env.get());
     coreChecker->setLogic(getLogicInfo());
     coreChecker->getOptions().smt.checkUnsatCores = false;
     // disable all proof options
@@ -1474,7 +1472,7 @@ void SmtEngine::checkUnsatCore() {
 
   // initialize the core checker
   std::unique_ptr<SmtEngine> coreChecker;
-  initializeSubsolver(coreChecker);
+  initializeSubsolver(coreChecker, *d_env.get());
   coreChecker->getOptions().smt.checkUnsatCores = false;
   // disable all proof options
   coreChecker->getOptions().smt.produceProofs = false;
@@ -1988,7 +1986,7 @@ std::string SmtEngine::getOption(const std::string& key) const
 
   if (Dump.isOn("benchmark"))
   {
-    getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key);
+    getPrinter().toStreamCmdGetOption(d_env->getDumpOut(), key);
   }
 
   if (key == "command-verbosity")
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 208c83db8..d9786f6a1 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -126,7 +126,7 @@ class CVC5_EXPORT SmtEngine
    * If provided, optr is a pointer to a set of options that should initialize the values
    * of the options object owned by this class.
    */
-  SmtEngine(NodeManager* nm, Options* optr = nullptr);
+  SmtEngine(NodeManager* nm, const Options* optr = nullptr);
   /** Destruct the SMT engine.  */
   ~SmtEngine();
 
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index d5cfe274e..b7b6d9c18 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -41,14 +41,11 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace smt {
 
-SygusSolver::SygusSolver(SmtSolver& sms,
-                         Preprocessor& pp,
-                         context::UserContext* u,
-                         OutputManager& outMgr)
-    : d_smtSolver(sms),
+SygusSolver::SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp)
+    : d_env(env),
+      d_smtSolver(sms),
       d_pp(pp),
-      d_sygusConjectureStale(u, true),
-      d_outMgr(outMgr)
+      d_sygusConjectureStale(env.getUserContext(), true)
 {
 }
 
@@ -212,7 +209,7 @@ Result SygusSolver::checkSynth(Assertions& as)
     Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
     if (Dump.isOn("raw-benchmark"))
     {
-      d_outMgr.getPrinter().toStreamCmdCheckSynth(d_outMgr.getDumpOut());
+      d_env.getPrinter().toStreamCmdCheckSynth(d_env.getDumpOut());
     }
 
     d_sygusConjectureStale = false;
@@ -332,7 +329,7 @@ void SygusSolver::checkSynthSolution(Assertions& as)
   {
     // Start new SMT engine to check solutions
     std::unique_ptr<SmtEngine> solChecker;
-    initializeSubsolver(solChecker);
+    initializeSubsolver(solChecker, d_env);
     solChecker->getOptions().smt.checkSynthSol = false;
     solChecker->getOptions().quantifiers.sygusRecFun = false;
     // get the solution for this conjecture
diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index ff9b7e513..82dfab3cc 100644
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -45,10 +45,7 @@ class SmtSolver;
 class SygusSolver
 {
  public:
-  SygusSolver(SmtSolver& sms,
-              Preprocessor& pp,
-              context::UserContext* u,
-              OutputManager& outMgr);
+  SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp);
   ~SygusSolver();
 
   /**
@@ -161,6 +158,8 @@ class SygusSolver
    * previously not stale.
    */
   void setSygusConjectureStale();
+  /** Reference to the env class */
+  Env& d_env;
   /** The SMT solver, which is used during checkSynth. */
   SmtSolver& d_smtSolver;
   /** The preprocessor, used for checkSynthSolution. */
@@ -180,8 +179,6 @@ class SygusSolver
    * Whether we need to reconstruct the sygus conjecture.
    */
   context::CDO<bool> d_sygusConjectureStale;
-  /** Reference to the output manager of the smt engine */
-  OutputManager& d_outMgr;
 };
 
 }  // namespace smt
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index f65828d2f..81366fabd 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -70,7 +70,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersState& qs,
   }
   if (options::cegqiNestedQE())
   {
-    d_nestedQe.reset(new NestedQe(qs.getUserContext()));
+    d_nestedQe.reset(new NestedQe(qs.getEnv()));
   }
 }
 
diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp
index a20c37043..869ebe036 100644
--- a/src/theory/quantifiers/cegqi/nested_qe.cpp
+++ b/src/theory/quantifiers/cegqi/nested_qe.cpp
@@ -18,13 +18,14 @@
 
 #include "expr/node_algorithm.h"
 #include "expr/subs.h"
+#include "smt/env.h"
 #include "theory/smt_engine_subsolver.h"
 
 namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-NestedQe::NestedQe(context::UserContext* u) : d_qnqe(u) {}
+NestedQe::NestedQe(Env& env) : d_env(env), d_qnqe(d_env.getUserContext()) {}
 
 bool NestedQe::process(Node q, std::vector<Node>& lems)
 {
@@ -35,7 +36,7 @@ bool NestedQe::process(Node q, std::vector<Node>& lems)
     return (*it).second != q;
   }
   Trace("cegqi-nested-qe") << "Check nested QE on " << q << std::endl;
-  Node qqe = doNestedQe(q, true);
+  Node qqe = doNestedQe(d_env, q, true);
   d_qnqe[q] = qqe;
   if (qqe == q)
   {
@@ -67,7 +68,7 @@ bool NestedQe::hasNestedQuantification(Node q)
   return getNestedQuantification(q, nqs);
 }
 
-Node NestedQe::doNestedQe(Node q, bool keepTopLevel)
+Node NestedQe::doNestedQe(Env& env, Node q, bool keepTopLevel)
 {
   NodeManager* nm = NodeManager::currentNM();
   Node qOrig = q;
@@ -88,7 +89,7 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel)
       return qOrig;
     }
     // just do ordinary quantifier elimination
-    Node qqe = doQe(q);
+    Node qqe = doQe(env, q);
     Trace("cegqi-nested-qe-debug") << "...did ordinary qe" << std::endl;
     return qqe;
   }
@@ -104,7 +105,7 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel)
   for (const Node& nq : nqs)
   {
     Node nqk = sk.apply(nq);
-    Node nqqe = doNestedQe(nqk);
+    Node nqqe = doNestedQe(env, nqk);
     if (nqqe == nqk)
     {
       // failed
@@ -130,14 +131,14 @@ Node NestedQe::doNestedQe(Node q, bool keepTopLevel)
   return nm->mkNode(inputExists ? kind::EXISTS : kind::FORALL, qargs);
 }
 
-Node NestedQe::doQe(Node q)
+Node NestedQe::doQe(Env& env, Node q)
 {
   Assert(q.getKind() == kind::FORALL);
   Trace("cegqi-nested-qe") << "  Apply qe to " << q << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   q = nm->mkNode(kind::EXISTS, q[0], q[1].negate());
   std::unique_ptr<SmtEngine> smt_qe;
-  initializeSubsolver(smt_qe);
+  initializeSubsolver(smt_qe, env);
   Node qqe = smt_qe->getQuantifierElimination(q, true, false);
   if (expr::hasBoundVar(qqe))
   {
diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h
index f6e15d4c6..f577a504c 100644
--- a/src/theory/quantifiers/cegqi/nested_qe.h
+++ b/src/theory/quantifiers/cegqi/nested_qe.h
@@ -25,6 +25,9 @@
 #include "expr/node.h"
 
 namespace cvc5 {
+
+class Env;
+
 namespace theory {
 namespace quantifiers {
 
@@ -33,7 +36,7 @@ class NestedQe
   using NodeNodeMap = context::CDHashMap<Node, Node>;
 
  public:
-  NestedQe(context::UserContext* u);
+  NestedQe(Env& env);
   ~NestedQe() {}
   /**
    * Process quantified formula. If this returns true, then q was processed
@@ -64,15 +67,17 @@ class NestedQe
    * returned formula is quantifier-free. Otherwise, it is a quantified formula
    * with no nested quantification.
    */
-  static Node doNestedQe(Node q, bool keepTopLevel = false);
+  static Node doNestedQe(Env& env, Node q, bool keepTopLevel = false);
   /**
    * Run quantifier elimination on quantified formula q, where q has no nested
    * quantification. This method invokes a subsolver for performing quantifier
    * elimination.
    */
-  static Node doQe(Node q);
+  static Node doQe(Env& env, Node q);
 
  private:
+  /** Reference to the env */
+  Env& d_env;
   /**
    * Mapping from quantified formulas q to the result of doNestedQe(q, true).
    */
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index fa156c839..49b1d56fa 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -56,12 +56,14 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
   Assert (!query.isNull());
   if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser)
   {
-    initializeSubsolver(
-        checker, nullptr, true, options::sygusExprMinerCheckTimeout());
+    initializeSubsolver(checker,
+                        d_env,
+                        true,
+                        options::sygusExprMinerCheckTimeout());
   }
   else
   {
-    initializeSubsolver(checker);
+    initializeSubsolver(checker, d_env);
   }
   // also set the options
   checker->setOption("sygus-rr-synth-input", "false");
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index f1caca1c4..99716806f 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -38,7 +38,8 @@ namespace theory {
 namespace quantifiers {
 
 CegSingleInv::CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s)
-    : d_sip(new SingleInvocationPartition),
+    : d_env(env),
+      d_sip(new SingleInvocationPartition),
       d_srcons(new SygusReconstruct(env, tr.getTermDatabaseSygus(), s)),
       d_isSolved(false),
       d_single_invocation(false),
@@ -227,7 +228,7 @@ bool CegSingleInv::solve()
   }
   // solve the single invocation conjecture using a fresh copy of SMT engine
   std::unique_ptr<SmtEngine> siSmt;
-  initializeSubsolver(siSmt);
+  initializeSubsolver(siSmt, d_env);
   siSmt->assertFormula(siq);
   Result r = siSmt->checkSat();
   Trace("sygus-si") << "Result: " << r << std::endl;
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index 13757dba9..f7d6e5bb9 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -51,6 +51,8 @@ class CegSingleInv
                                std::map< Node, std::vector< Node > >& teq,
                                Node n, std::vector< Node >& conj );
  private:
+  /** Reference to the env */
+  Env& d_env;
   // single invocation inference utility
   SingleInvocationPartition* d_sip;
   /** solution reconstruction */
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index dff44eb1c..57b763044 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -32,10 +32,11 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-Cegis::Cegis(QuantifiersInferenceManager& qim,
+Cegis::Cegis(QuantifiersState& qs,
+             QuantifiersInferenceManager& qim,
              TermDbSygus* tds,
              SynthConjecture* p)
-    : SygusModule(qim, tds, p),
+    : SygusModule(qs, qim, tds, p),
       d_eval_unfold(tds->getEvalUnfold()),
       d_usingSymCons(false)
 {
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index f5114d7ca..d6678a305 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -42,7 +42,10 @@ namespace quantifiers {
 class Cegis : public SygusModule
 {
  public:
-  Cegis(QuantifiersInferenceManager& qim, TermDbSygus* tds, SynthConjecture* p);
+  Cegis(QuantifiersState& qs,
+        QuantifiersInferenceManager& qim,
+        TermDbSygus* tds,
+        SynthConjecture* p);
   ~Cegis() override {}
   /** initialize */
   virtual bool initialize(Node conj,
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 165326db7..9a9d8f02d 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -68,10 +68,11 @@ bool VariadicTrie::hasSubset(const std::vector<Node>& is) const
   return false;
 }
 
-CegisCoreConnective::CegisCoreConnective(QuantifiersInferenceManager& qim,
+CegisCoreConnective::CegisCoreConnective(QuantifiersState& qs,
+                                         QuantifiersInferenceManager& qim,
                                          TermDbSygus* tds,
                                          SynthConjecture* p)
-    : Cegis(qim, tds, p)
+    : Cegis(qs, qim, tds, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
@@ -628,7 +629,9 @@ bool CegisCoreConnective::getUnsatCore(
 Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const
 {
   Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl;
-  Result r = checkWithSubsolver(n, d_vars, mvs);
+  Env& env = d_qstate.getEnv();
+  Result r =
+      checkWithSubsolver(n, d_vars, mvs, env.getOptions(), env.getLogicInfo());
   Trace("sygus-ccore-debug") << "...got " << r << std::endl;
   return r;
 }
@@ -736,7 +739,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
     addSuccess = false;
     // try a new core
     std::unique_ptr<SmtEngine> checkSol;
-    initializeSubsolver(checkSol);
+    initializeSubsolver(checkSol, d_qstate.getEnv());
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
     rasserts.push_back(d_sc);
@@ -776,7 +779,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
           // In terms of Variant #2, this is the check "if S ^ U is unsat"
           Trace("sygus-ccore") << "----- Check side condition" << std::endl;
           std::unique_ptr<SmtEngine> checkSc;
-          initializeSubsolver(checkSc);
+          initializeSubsolver(checkSc, d_qstate.getEnv());
           std::vector<Node> scasserts;
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
           scasserts.push_back(d_sc);
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index 005e85706..e9a73e9bb 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -160,7 +160,8 @@ class VariadicTrie
 class CegisCoreConnective : public Cegis
 {
  public:
-  CegisCoreConnective(QuantifiersInferenceManager& qim,
+  CegisCoreConnective(QuantifiersState& qs,
+                      QuantifiersInferenceManager& qim,
                       TermDbSygus* tds,
                       SynthConjecture* p);
   ~CegisCoreConnective() {}
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 0b7255e2d..c4d9cbd4a 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -34,7 +34,7 @@ CegisUnif::CegisUnif(QuantifiersState& qs,
                      QuantifiersInferenceManager& qim,
                      TermDbSygus* tds,
                      SynthConjecture* p)
-    : Cegis(qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p)
+    : Cegis(qs, qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p)
 {
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 426ad07ef..0dad29893 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -22,6 +22,7 @@
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "options/smt_options.h"
+#include "smt/env.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
@@ -32,7 +33,7 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusInterpol::SygusInterpol() {}
+SygusInterpol::SygusInterpol(Env& env) : d_env(env) {}
 
 void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
                                    const Node& conj)
@@ -324,7 +325,7 @@ bool SygusInterpol::solveInterpolation(const std::string& name,
   mkSygusConjecture(itp, axioms, conj);
 
   std::unique_ptr<SmtEngine> subSolver;
-  initializeSubsolver(subSolver);
+  initializeSubsolver(subSolver, d_env);
   // get the logic
   LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy();
   // enable everything needed for sygus
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index e86ac624a..d4aedad8a 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -25,6 +25,7 @@
 
 namespace cvc5 {
 
+class Env;
 class SmtEngine;
 
 namespace theory {
@@ -61,7 +62,7 @@ namespace quantifiers {
 class SygusInterpol
 {
  public:
-  SygusInterpol();
+  SygusInterpol(Env& env);
 
   /**
    * Returns the sygus conjecture in interpol corresponding to the interpolation
@@ -173,7 +174,8 @@ class SygusInterpol
    * @param itp the interpolation predicate.
    */
   bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp);
-
+  /** Reference to the env */
+  Env& d_env;
   /**
    * symbols from axioms and conjecture.
    */
diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index b134eb993..4cb333849 100644
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -19,10 +19,11 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusModule::SygusModule(QuantifiersInferenceManager& qim,
+SygusModule::SygusModule(QuantifiersState& qs,
+                         QuantifiersInferenceManager& qim,
                          TermDbSygus* tds,
                          SynthConjecture* p)
-    : d_qim(qim), d_tds(tds), d_parent(p)
+    : d_qstate(qs), d_qim(qim), d_tds(tds), d_parent(p)
 {
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index d93957a15..d7e0caa5b 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -28,6 +28,7 @@ namespace quantifiers {
 
 class SynthConjecture;
 class TermDbSygus;
+class QuantifiersState;
 class QuantifiersInferenceManager;
 
 /** SygusModule
@@ -51,7 +52,8 @@ class QuantifiersInferenceManager;
 class SygusModule
 {
  public:
-  SygusModule(QuantifiersInferenceManager& qim,
+  SygusModule(QuantifiersState& qs,
+              QuantifiersInferenceManager& qim,
               TermDbSygus* tds,
               SynthConjecture* p);
   virtual ~SygusModule() {}
@@ -147,6 +149,8 @@ class SygusModule
   virtual bool usingRepairConst() { return false; }
 
  protected:
+  /** Reference to the state of the quantifiers engine */
+  QuantifiersState& d_qstate;
   /** Reference to the quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
   /** sygus term database of d_qe */
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 27a1e3f3b..26621eb96 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -30,10 +30,11 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusPbe::SygusPbe(QuantifiersInferenceManager& qim,
+SygusPbe::SygusPbe(QuantifiersState& qs,
+                   QuantifiersInferenceManager& qim,
                    TermDbSygus* tds,
                    SynthConjecture* p)
-    : SygusModule(qim, tds, p)
+    : SygusModule(qs, qim, tds, p)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index e27f4ce35..867764617 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -86,7 +86,8 @@ class SynthConjecture;
 class SygusPbe : public SygusModule
 {
  public:
-  SygusPbe(QuantifiersInferenceManager& qim,
+  SygusPbe(QuantifiersState& qs,
+           QuantifiersInferenceManager& qim,
            TermDbSygus* tds,
            SynthConjecture* p);
   ~SygusPbe();
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
index c6ff7e61a..5cf7122f3 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
@@ -27,7 +27,7 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SygusQePreproc::SygusQePreproc() {}
+SygusQePreproc::SygusQePreproc(Env& env) : d_env(env) {}
 
 Node SygusQePreproc::preprocess(Node q)
 {
@@ -53,7 +53,7 @@ Node SygusQePreproc::preprocess(Node q)
   }
   // create new smt engine to do quantifier elimination
   std::unique_ptr<SmtEngine> smt_qe;
-  initializeSubsolver(smt_qe);
+  initializeSubsolver(smt_qe, d_env);
   Trace("cegqi-qep") << "Property is non-ground single invocation, run "
                         "QE to obtain single invocation."
                      << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
index 551dd1611..0cbd96914 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
@@ -19,6 +19,9 @@
 #include "expr/node.h"
 
 namespace cvc5 {
+
+class Env;
+
 namespace theory {
 namespace quantifiers {
 
@@ -35,13 +38,17 @@ namespace quantifiers {
 class SygusQePreproc
 {
  public:
-  SygusQePreproc();
+  SygusQePreproc(Env& env);
   ~SygusQePreproc() {}
   /**
    * Preprocess. Returns a lemma of the form q = nq where nq is obtained
    * by the quantifier elimination technique outlined above.
    */
   Node preprocess(Node q);
+
+ private:
+  /** Reference to the env */
+  Env& d_env;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index d4611e6ca..4a8d0406b 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -232,7 +232,8 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
   // initialize the subsolver using the standard method
   initializeSubsolver(
       repcChecker,
-      nullptr,
+      d_env.getOptions(),
+      d_env.getLogicInfo(),
       Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
       options::sygusRepairConstTimeout());
   // renable options disabled by sygus
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index eeadbdd54..3e7095c12 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -56,7 +56,7 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs,
       d_treg(tr),
       d_stats(s),
       d_tds(tr.getTermDatabaseSygus()),
-      d_verify(qs.options(), d_tds),
+      d_verify(qs.options(), qs.getLogicInfo(), d_tds),
       d_hasSolution(false),
       d_ceg_si(new CegSingleInv(qs.getEnv(), tr, s)),
       d_templInfer(new SygusTemplateInfer),
@@ -64,10 +64,10 @@ SynthConjecture::SynthConjecture(QuantifiersState& qs,
       d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
       d_sygus_rconst(new SygusRepairConst(qs.getEnv(), d_tds)),
       d_exampleInfer(new ExampleInfer(d_tds)),
-      d_ceg_pbe(new SygusPbe(qim, d_tds, this)),
-      d_ceg_cegis(new Cegis(qim, d_tds, this)),
+      d_ceg_pbe(new SygusPbe(qs, qim, d_tds, this)),
+      d_ceg_cegis(new Cegis(qs, qim, d_tds, this)),
       d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)),
-      d_sygus_ccore(new CegisCoreConnective(qim, d_tds, this)),
+      d_sygus_ccore(new CegisCoreConnective(qs, qim, d_tds, this)),
       d_master(nullptr),
       d_set_ce_sk_vars(false),
       d_repair_index(0),
@@ -609,7 +609,8 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const
     }
     Trace("sygus-engine") << "Check side condition..." << std::endl;
     Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
-    Result r = checkWithSubsolver(sc);
+    Env& env = d_qstate.getEnv();
+    Result r = checkWithSubsolver(sc, env.getOptions(), env.getLogicInfo());
     Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
     if (r == Result::UNSAT)
     {
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 65907cb31..cdcbeb85d 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -30,7 +30,7 @@ SynthEngine::SynthEngine(QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
                          TermRegistry& tr)
-    : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp()
+    : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp(qs.getEnv())
 {
   d_conjs.push_back(std::unique_ptr<SynthConjecture>(
       new SynthConjecture(qs, qim, qr, tr, d_statistics)));
diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp
index 9e8171fdc..db09b45ed 100644
--- a/src/theory/quantifiers/sygus/synth_verify.cpp
+++ b/src/theory/quantifiers/sygus/synth_verify.cpp
@@ -32,7 +32,10 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-SynthVerify::SynthVerify(const Options& opts, TermDbSygus* tds) : d_tds(tds)
+SynthVerify::SynthVerify(const Options& opts,
+                         const LogicInfo& logicInfo,
+                         TermDbSygus* tds)
+    : d_tds(tds), d_subLogicInfo(logicInfo)
 {
   // determine the options to use for the verification subsolvers we spawn
   // we start with the provided options
@@ -102,7 +105,7 @@ Result SynthVerify::verify(Node query,
     }
   }
   Trace("sygus-engine") << "  *** Verify with subcall..." << std::endl;
-  Result r = checkWithSubsolver(query, vars, mvs, &d_subOptions);
+  Result r = checkWithSubsolver(query, vars, mvs, d_subOptions, d_subLogicInfo);
   Trace("sygus-engine") << "  ...got " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() == Result::SAT)
   {
diff --git a/src/theory/quantifiers/sygus/synth_verify.h b/src/theory/quantifiers/sygus/synth_verify.h
index c4d1052da..948a70787 100644
--- a/src/theory/quantifiers/sygus/synth_verify.h
+++ b/src/theory/quantifiers/sygus/synth_verify.h
@@ -34,7 +34,9 @@ namespace quantifiers {
 class SynthVerify
 {
  public:
-  SynthVerify(const Options& opts, TermDbSygus* tds);
+  SynthVerify(const Options& opts,
+              const LogicInfo& logicInfo,
+              TermDbSygus* tds);
   ~SynthVerify();
   /**
    * Verification call, which takes into account specific aspects of the
@@ -55,6 +57,8 @@ class SynthVerify
   TermDbSygus* d_tds;
   /** The options for subsolver calls */
   Options d_subOptions;
+  /** The logic info for subsolver calls */
+  const LogicInfo& d_subLogicInfo;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 5f285dc07..dda065d7b 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/smt_engine_subsolver.h"
 
+#include "smt/env.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/rewriter.h"
@@ -42,30 +43,34 @@ Result quickCheck(Node& query)
 }
 
 void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
-                         Options* opts,
+                         const Options& opts,
+                         const LogicInfo& logicInfo,
                          bool needsTimeout,
                          unsigned long timeout)
 {
   NodeManager* nm = NodeManager::currentNM();
-  SmtEngine* smtCurr = smt::currentSmtEngine();
-  if (opts == nullptr)
-  {
-    // must copy the options
-    opts = &smtCurr->getOptions();
-  }
-  smte.reset(new SmtEngine(nm, opts));
+  smte.reset(new SmtEngine(nm, &opts));
   smte->setIsInternalSubsolver();
-  smte->setLogic(smtCurr->getLogicInfo());
+  smte->setLogic(logicInfo);
   // set the options
   if (needsTimeout)
   {
     smte->setTimeLimit(timeout);
   }
 }
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+                         const Env& env,
+                         bool needsTimeout,
+                         unsigned long timeout)
+{
+  initializeSubsolver(
+      smte, env.getOptions(), env.getLogicInfo(), needsTimeout, timeout);
+}
 
 Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
                           Node query,
-                          Options* opts,
+                          const Options& opts,
+                          const LogicInfo& logicInfo,
                           bool needsTimeout,
                           unsigned long timeout)
 {
@@ -75,26 +80,28 @@ Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
   {
     return r;
   }
-  initializeSubsolver(smte, opts, needsTimeout, timeout);
+  initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout);
   smte->assertFormula(query);
   return smte->checkSat();
 }
 
 Result checkWithSubsolver(Node query,
-                          Options* opts,
+                          const Options& opts,
+                          const LogicInfo& logicInfo,
                           bool needsTimeout,
                           unsigned long timeout)
 {
   std::vector<Node> vars;
   std::vector<Node> modelVals;
   return checkWithSubsolver(
-      query, vars, modelVals, opts, needsTimeout, timeout);
+      query, vars, modelVals, opts, logicInfo, needsTimeout, timeout);
 }
 
 Result checkWithSubsolver(Node query,
                           const std::vector<Node>& vars,
                           std::vector<Node>& modelVals,
-                          Options* opts,
+                          const Options& opts,
+                          const LogicInfo& logicInfo,
                           bool needsTimeout,
                           unsigned long timeout)
 {
@@ -116,7 +123,7 @@ Result checkWithSubsolver(Node query,
     return r;
   }
   std::unique_ptr<SmtEngine> smte;
-  initializeSubsolver(smte, opts, needsTimeout, timeout);
+  initializeSubsolver(smte, opts, logicInfo, needsTimeout, timeout);
   smte->assertFormula(query);
   r = smte->checkSat();
   if (r.asSatisfiabilityResult().isSat() == Result::SAT)
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index 2d80831f2..028c35cd8 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -41,13 +41,22 @@ namespace theory {
  * if the current SMT engine has declared a separation logic heap.
  *
  * @param smte The smt engine pointer to initialize
- * @param opts The options for the subsolver. If nullptr, then we copy the
- * options from the current SmtEngine in scope.
+ * @param opts The options for the subsolver.
+ * @param logicInfo The logic info to set on the subsolver
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
 void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
-                         Options* opts = nullptr,
+                         const Options& opts,
+                         const LogicInfo& logicInfo,
+                         bool needsTimeout = false,
+                         unsigned long timeout = 0);
+
+/**
+ * Version that uses the options and logicInfo in an environment.
+ */
+void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
+                         const Env& env,
                          bool needsTimeout = false,
                          unsigned long timeout = 0);
 
@@ -59,7 +68,8 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
  */
 Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
                           Node query,
-                          Options* opts = nullptr,
+                          const Options& opts,
+                          const LogicInfo& logicInfo,
                           bool needsTimeout = false,
                           unsigned long timeout = 0);
 
@@ -71,11 +81,13 @@ Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte,
  *
  * @param query The query to check
  * @param opts The options for the subsolver
+ * @param logicInfo The logic info to set on the subsolver
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
 Result checkWithSubsolver(Node query,
-                          Options* opts = nullptr,
+                          const Options& opts,
+                          const LogicInfo& logicInfo,
                           bool needsTimeout = false,
                           unsigned long timeout = 0);
 
@@ -88,13 +100,15 @@ Result checkWithSubsolver(Node query,
  * @param vars The variables we are interesting in getting a model for.
  * @param modelVals A vector storing the model values of variables in vars.
  * @param opts The options for the subsolver
+ * @param logicInfo The logic info to set on the subsolver
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
 Result checkWithSubsolver(Node query,
                           const std::vector<Node>& vars,
                           std::vector<Node>& modelVals,
-                          Options* opts = nullptr,
+                          const Options& opts,
+                          const LogicInfo& logicInfo,
                           bool needsTimeout = false,
                           unsigned long timeout = 0);