Split SmtSolver from SmtEngine (#4880)

This class is responsible for maintaining TheoryEngine and PropEngine and implementing the check-sat command. It also has an interface for processing/pushing the current assertions into the PropEngine.

This class will be used directly by other extension solvers (for abduction, interpolation, qe, sygus, etc.).

9 files changed, 546 insertions, 293 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 77c363317..1f7f68289 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -267,6 +267,8 @@ libcvc4_add_sources(
   smt/smt_engine_stats.h
   smt/smt_mode.cpp
   smt/smt_mode.h
+  smt/smt_solver.cpp
+  smt/smt_solver.h
   smt/smt_statistics_registry.cpp
   smt/smt_statistics_registry.h
   smt/term_formula_removal.cpp
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 492f3e105..4da13f108 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -504,7 +504,9 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions)
     Debug("smt") << " assertions     : " << assertions.size() << endl;
 
     // before ppRewrite check if only core theory for BV theory
-    d_smt.d_theoryEngine->staticInitializeBVOptions(assertions.ref());
+    TheoryEngine* te = d_smt.getTheoryEngine();
+    Assert(te != nullptr);
+    te->staticInitializeBVOptions(assertions.ref());
 
     // Theory preprocessing
     bool doEarlyTheoryPp = !options::arithRewriteEq();
@@ -735,7 +737,7 @@ Node ProcessAssertions::expandDefinitions(
       {
         // do not do any theory stuff if expandOnly is true
 
-        theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node);
+        theory::Theory* t = d_smt.getTheoryEngine()->theoryOf(node);
 
         Assert(t != NULL);
         TrustNode trn = t->expandDefinition(n);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7374c8ca9..e709406d8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -79,7 +79,6 @@
 #include "proof/proof_manager.h"
 #include "proof/theory_proof.h"
 #include "proof/unsat_core.h"
-#include "prop/prop_engine.h"
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
@@ -96,6 +95,7 @@
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_engine_state.h"
 #include "smt/smt_engine_stats.h"
+#include "smt/smt_solver.h"
 #include "smt/term_formula_removal.h"
 #include "smt/update_ostream.h"
 #include "smt_util/boolean_simplification.h"
@@ -202,8 +202,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_dumpm(new DumpManager(getUserContext())),
       d_routListener(new ResourceOutListener(*this)),
       d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())),
-      d_theoryEngine(nullptr),
-      d_propEngine(nullptr),
+      d_smtSolver(nullptr),
       d_proofManager(nullptr),
       d_rewriter(new theory::Rewriter()),
       d_definedFunctions(nullptr),
@@ -253,7 +252,10 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
   d_resourceManager->registerListener(d_routListener.get());
   // make statistics
   d_stats.reset(new SmtEngineStatistics());
-  
+  // make the SMT solver
+  d_smtSolver.reset(
+      new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats));
+
   // The ProofManager is constructed before any other proof objects such as
   // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
   // initialized in TheoryEngine and PropEngine respectively.
@@ -286,6 +288,16 @@ context::UserContext* SmtEngine::getUserContext()
 }
 context::Context* SmtEngine::getContext() { return d_state->getContext(); }
 
+TheoryEngine* SmtEngine::getTheoryEngine()
+{
+  return d_smtSolver->getTheoryEngine();
+}
+
+prop::PropEngine* SmtEngine::getPropEngine()
+{
+  return d_smtSolver->getPropEngine();
+}
+
 void SmtEngine::finishInit()
 {
   if (d_state->isFullyInited())
@@ -313,37 +325,7 @@ void SmtEngine::finishInit()
   d_optm->finishInit(d_logic, d_isInternalSubsolver);
 
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
-  // We have mutual dependency here, so we add the prop engine to the theory
-  // engine later (it is non-essential there)
-  d_theoryEngine.reset(new TheoryEngine(getContext(),
-                                        getUserContext(),
-                                        getResourceManager(),
-                                        d_pp->getTermFormulaRemover(),
-                                        const_cast<const LogicInfo&>(d_logic)));
-
-  // Add the theories
-  for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
-    TheoryConstructor::addTheory(getTheoryEngine(), id);
-    //register with proof engine if applicable
-#ifdef CVC4_PROOF
-    ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id));
-#endif
-  }
-
-  Trace("smt-debug") << "Making decision engine..." << std::endl;
-
-  Trace("smt-debug") << "Making prop engine..." << std::endl;
-  /* force destruction of referenced PropEngine to enforce that statistics
-   * are unregistered by the obsolete PropEngine object before registered
-   * again by the new PropEngine object */
-  d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(
-      getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
-
-  Trace("smt-debug") << "Setting up theory engine..." << std::endl;
-  d_theoryEngine->setPropEngine(getPropEngine());
-  Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
-  d_theoryEngine->finishInit();
+  d_smtSolver->finishInit(const_cast<const LogicInfo&>(d_logic));
 
   // global push/pop around everything, to ensure proper destruction
   // of context-dependent data structures
@@ -377,14 +359,16 @@ void SmtEngine::finishInit()
 
   PROOF( ProofManager::currentPM()->setLogic(d_logic); );
   PROOF({
-      for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
-        ProofManager::currentPM()->getTheoryProofEngine()->
-          finishRegisterTheory(d_theoryEngine->theoryOf(id));
-      }
-    });
+    TheoryEngine* te = d_smtSolver->getTheoryEngine();
+    for (TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id)
+    {
+      ProofManager::currentPM()->getTheoryProofEngine()->finishRegisterTheory(
+          te->theoryOf(id));
+    }
+  });
   d_pp->finishInit();
 
-  AlwaysAssert(d_propEngine->getAssertionLevel() == 0)
+  AlwaysAssert(getPropEngine()->getAssertionLevel() == 0)
       << "The PropEngine has pushed but the SmtEngine "
          "hasn't finished initializing!";
 
@@ -398,14 +382,7 @@ void SmtEngine::finishInit()
 void SmtEngine::shutdown() {
   d_state->shutdown();
 
-  if (d_propEngine != nullptr)
-  {
-    d_propEngine->shutdown();
-  }
-  if (d_theoryEngine != nullptr)
-  {
-    d_theoryEngine->shutdown();
-  }
+  d_smtSolver->shutdown();
 }
 
 SmtEngine::~SmtEngine()
@@ -444,8 +421,7 @@ SmtEngine::~SmtEngine()
     d_exprNames.reset(nullptr);
     d_dumpm.reset(nullptr);
 
-    d_theoryEngine.reset(nullptr);
-    d_propEngine.reset(nullptr);
+    d_smtSolver.reset(nullptr);
 
     d_stats.reset(nullptr);
     d_private.reset(nullptr);
@@ -925,40 +901,6 @@ bool SmtEngine::isDefinedFunction( Expr func ){
   return d_definedFunctions->find(nf) != d_definedFunctions->end();
 }
 
-Result SmtEngine::check() {
-  Assert(d_state->isFullyReady());
-
-  Trace("smt") << "SmtEngine::check()" << endl;
-
-  const std::string& filename = d_state->getFilename();
-  if (d_resourceManager->out())
-  {
-    Result::UnknownExplanation why = d_resourceManager->outOfResources()
-                                         ? Result::RESOURCEOUT
-                                         : Result::TIMEOUT;
-    return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
-  }
-  d_resourceManager->beginCall();
-
-  // Make sure the prop layer has all of the assertions
-  Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
-  processAssertionsInternal();
-  Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
-
-  TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
-
-  Chat() << "solving..." << endl;
-  Trace("smt") << "SmtEngine::check(): running check" << endl;
-  Result result = d_propEngine->checkSat();
-
-  d_resourceManager->endCall();
-  Trace("limit") << "SmtEngine::check(): cumulative millis "
-                 << d_resourceManager->getTimeUsage() << ", resources "
-                 << d_resourceManager->getResourceUsage() << endl;
-
-  return Result(result, filename);
-}
-
 Result SmtEngine::quickCheck() {
   Assert(d_state->isFullyInited());
   Trace("smt") << "SMT quickCheck()" << endl;
@@ -993,7 +935,9 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
     throw ModalException(ss.str().c_str());
   }
 
-  TheoryModel* m = d_theoryEngine->getBuiltModel();
+  TheoryEngine* te = d_smtSolver->getTheoryEngine();
+  Assert(te != nullptr);
+  TheoryModel* m = te->getBuiltModel();
 
   if (m == nullptr)
   {
@@ -1007,71 +951,46 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
   return m;
 }
 
-void SmtEngine::notifyPushPre() { processAssertionsInternal(); }
+void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); }
+
 void SmtEngine::notifyPushPost()
 {
   TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
-  d_propEngine->push();
+  Assert(getPropEngine() != nullptr);
+  getPropEngine()->push();
 }
+
 void SmtEngine::notifyPopPre()
 {
   TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
-  d_propEngine->pop();
+  PropEngine* pe = getPropEngine();
+  Assert(pe != nullptr);
+  pe->pop();
 }
-void SmtEngine::notifyPostSolvePre() { d_propEngine->resetTrail(); }
-void SmtEngine::notifyPostSolvePost() { d_theoryEngine->postsolve(); }
 
-void SmtEngine::processAssertionsInternal()
+void SmtEngine::notifyPostSolvePre()
 {
-  TimerStat::CodeTimer paTimer(d_stats->d_processAssertionsTime);
-  d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep);
-  Assert(d_state->isFullyReady());
-
-  AssertionPipeline& ap = d_asserts->getAssertionPipeline();
-
-  if (ap.size() == 0)
-  {
-    // nothing to do
-    return;
-  }
-
-  // process the assertions with the preprocessor
-  bool noConflict = d_pp->process(*d_asserts);
-
-  //notify theory engine new preprocessed assertions
-  d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
-
-  // Push the formula to decision engine
-  if (noConflict)
-  {
-    Chat() << "pushing to decision engine..." << endl;
-    d_propEngine->addAssertionsToDecisionEngine(ap);
-  }
-
-  // end: INVARIANT to maintain: no reordering of assertions or
-  // introducing new ones
-
-  d_pp->postprocess(*d_asserts);
-
-  // Push the formula to SAT
-  {
-    Chat() << "converting to CNF..." << endl;
-    TimerStat::CodeTimer codeTimer(d_stats->d_cnfConversionTime);
-    for (const Node& assertion : ap.ref())
-    {
-      Chat() << "+ " << assertion << std::endl;
-      d_propEngine->assertFormula(assertion);
-    }
-  }
+  PropEngine* pe = getPropEngine();
+  Assert(pe != nullptr);
+  pe->resetTrail();
+}
 
-  // clear the current assertions
-  d_asserts->clearCurrent();
+void SmtEngine::notifyPostSolvePost()
+{
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
+  te->postsolve();
 }
 
 Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
 {
   Dump("benchmark") << CheckSatCommand(assumption);
-  return checkSatisfiability(Node::fromExpr(assumption), inUnsatCore, false);
+  std::vector<Node> assump;
+  if (!assumption.isNull())
+  {
+    assump.push_back(Node::fromExpr(assumption));
+  }
+  return checkSatInternal(assump, inUnsatCore, false);
 }
 
 Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
@@ -1089,17 +1008,17 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
   {
     assumps.push_back(Node::fromExpr(e));
   }
-  return checkSatisfiability(assumps, inUnsatCore, false);
+  return checkSatInternal(assumps, inUnsatCore, false);
 }
 
 Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore)
 {
   Dump("benchmark") << QueryCommand(node, inUnsatCore);
-  return checkSatisfiability(node.isNull()
-                                 ? std::vector<Node>()
-                                 : std::vector<Node>{Node::fromExpr(node)},
-                             inUnsatCore,
-                             true)
+  return checkSatInternal(node.isNull()
+                              ? std::vector<Node>()
+                              : std::vector<Node>{Node::fromExpr(node)},
+                          inUnsatCore,
+                          true)
       .asEntailmentResult();
 }
 
@@ -1110,22 +1029,12 @@ Result SmtEngine::checkEntailed(const vector<Expr>& nodes, bool inUnsatCore)
   {
     ns.push_back(Node::fromExpr(e));
   }
-  return checkSatisfiability(ns, inUnsatCore, true).asEntailmentResult();
+  return checkSatInternal(ns, inUnsatCore, true).asEntailmentResult();
 }
 
-Result SmtEngine::checkSatisfiability(const Node& node,
-                                      bool inUnsatCore,
-                                      bool isEntailmentCheck)
-{
-  return checkSatisfiability(
-      node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
-      inUnsatCore,
-      isEntailmentCheck);
-}
-
-Result SmtEngine::checkSatisfiability(const vector<Node>& assumptions,
-                                      bool inUnsatCore,
-                                      bool isEntailmentCheck)
+Result SmtEngine::checkSatInternal(const vector<Node>& assumptions,
+                                   bool inUnsatCore,
+                                   bool isEntailmentCheck)
 {
   try
   {
@@ -1135,46 +1044,9 @@ Result SmtEngine::checkSatisfiability(const vector<Node>& assumptions,
     Trace("smt") << "SmtEngine::"
                  << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "("
                  << assumptions << ")" << endl;
-    // update the state to indicate we are about to run a check-sat
-    bool hasAssumptions = !assumptions.empty();
-    d_state->notifyCheckSat(hasAssumptions);
-
-    // then, initialize the assertions
-    d_asserts->initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
-
-    // make the check
-    Result r = check();
-
-    if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
-        && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
-    {
-      r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
-    }
-    // flipped if we did a global negation
-    if (d_asserts->isGlobalNegated())
-    {
-      Trace("smt") << "SmtEngine::process global negate " << r << std::endl;
-      if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
-      {
-        r = Result(Result::SAT);
-      }
-      else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
-      {
-        // only if satisfaction complete
-        if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
-        {
-          r = Result(Result::UNSAT);
-        }
-        else
-        {
-          r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
-        }
-      }
-      Trace("smt") << "SmtEngine::global negate returned " << r << std::endl;
-    }
-
-    // notify our state of the check-sat result
-    d_state->notifyCheckSatResult(hasAssumptions, r);
+    // check the satisfiability with the solver object
+    Result r = d_smtSolver->checkSatisfiability(
+        *d_asserts.get(), assumptions, inUnsatCore, isEntailmentCheck);
 
     Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
                  << "(" << assumptions << ") => " << r << endl;
@@ -1456,7 +1328,7 @@ Result SmtEngine::checkSynth()
     throw ModalException(
         "Cannot make check-synth commands when incremental solving is enabled");
   }
-  Expr query;
+  std::vector<Node> query;
   if (d_private->d_sygusConjectureStale)
   {
     // build synthesis conjecture from asserted constraints and declared
@@ -1500,10 +1372,10 @@ Result SmtEngine::checkSynth()
     d_private->d_sygusConjectureStale = false;
 
     // TODO (project #7): if incremental, we should push a context and assert
-    query = body.toExpr();
+    query.push_back(body);
   }
 
-  Result r = checkSatisfiability(query, true, false);
+  Result r = checkSatInternal(query, true, false);
 
   // Check that synthesis solutions satisfy the conjecture
   if (options::checkSynthSol()
@@ -1526,7 +1398,7 @@ Node SmtEngine::simplify(const Node& ex)
   finishInit();
   d_state->doPendingPops();
   // ensure we've processed assertions
-  processAssertionsInternal();
+  d_smtSolver->processAssertions(*d_asserts);
   return d_pp->simplify(ex);
 }
 
@@ -1715,7 +1587,9 @@ Model* SmtEngine::getModel() {
   // Since model m is being returned to the user, we must ensure that this
   // model object remains valid with future check-sat calls. Hence, we set
   // the theory engine into "eager model building" mode. TODO #2648: revisit.
-  d_theoryEngine->setEagerModelBuilding();
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
+  te->setEagerModelBuilding();
 
   if (options::modelCoresMode() != options::ModelCoresMode::NONE)
   {
@@ -1956,7 +1830,9 @@ void SmtEngine::checkModel(bool hardFailure) {
   // Check individual theory assertions
   if (options::debugCheckModels())
   {
-    d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure);
+    TheoryEngine* te = getTheoryEngine();
+    Assert(te != nullptr);
+    te->checkTheoryAssertionsWithModel(hardFailure);
   }
   
   // Output the model
@@ -2161,8 +2037,10 @@ void SmtEngine::checkSynthSolution()
   NodeManager* nm = NodeManager::currentNM();
   Notice() << "SmtEngine::checkSynthSolution(): checking synthesis solution" << endl;
   std::map<Node, std::map<Node, Node>> sol_map;
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
   /* Get solutions and build auxiliary vectors for substituting */
-  if (!d_theoryEngine->getSynthSolutions(sol_map))
+  if (!te->getSynthSolutions(sol_map))
   {
     InternalError() << "SmtEngine::checkSynthSolution(): No solution to check!";
     return;
@@ -2353,11 +2231,9 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
     out << "% SZS output start Proof for " << d_state->getFilename()
         << std::endl;
   }
-  if( d_theoryEngine ){
-    d_theoryEngine->printInstantiations( out );
-  }else{
-    Assert(false);
-  }
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
+  te->printInstantiations(out);
   if (options::instFormatMode() == options::InstFormatMode::SZS)
   {
     out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
@@ -2367,11 +2243,9 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
 void SmtEngine::printSynthSolution( std::ostream& out ) {
   SmtScope smts(this);
   finishInit();
-  if( d_theoryEngine ){
-    d_theoryEngine->printSynthSolution( out );
-  }else{
-    Assert(false);
-  }
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
+  te->printSynthSolution(out);
 }
 
 bool SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map)
@@ -2379,9 +2253,10 @@ bool SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map)
   SmtScope smts(this);
   finishInit();
   std::map<Node, std::map<Node, Node>> sol_mapn;
-  Assert(d_theoryEngine != nullptr);
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
   // fail if the theory engine does not have synthesis solutions
-  if (!d_theoryEngine->getSynthSolutions(sol_mapn))
+  if (!te->getSynthSolutions(sol_mapn))
   {
     return false;
   }
@@ -2413,7 +2288,10 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
   TypeNode t = NodeManager::currentNM()->booleanType();
   Node n_attr = NodeManager::currentNM()->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
   std::vector< Node > node_values;
-  d_theoryEngine->setUserAttribute( doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
+  te->setUserAttribute(
+      doFull ? "quant-elim" : "quant-elim-partial", n_attr, node_values, "");
   n_attr = NodeManager::currentNM()->mkNode(kind::INST_ATTRIBUTE, n_attr);
   n_attr = NodeManager::currentNM()->mkNode(kind::INST_PATTERN_LIST, n_attr);
   std::vector< Node > e_children;
@@ -2424,7 +2302,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
   Node nn_e = NodeManager::currentNM()->mkNode( kind::EXISTS, e_children );
   Trace("smt-qe-debug") << "Query for quantifier elimination : " << nn_e << std::endl;
   Assert(nn_e.getNumChildren() == 3);
-  Result r = checkSatisfiability(nn_e.toExpr(), true, true);
+  Result r = checkSatInternal(std::vector<Node>{nn_e}, true, true);
   Trace("smt-qe") << "Query returned " << r << std::endl;
   if(r.asSatisfiabilityResult().isSat() != Result::UNSAT ) {
     if( r.asSatisfiabilityResult().isSat() != Result::SAT && doFull ){
@@ -2435,7 +2313,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
       return e;
     }
     std::vector< Node > inst_qs;
-    d_theoryEngine->getInstantiatedQuantifiedFormulas( inst_qs );
+    te->getInstantiatedQuantifiedFormulas(inst_qs);
     Assert(inst_qs.size() <= 1);
     Node ret_n;
     if( inst_qs.size()==1 ){
@@ -2443,7 +2321,7 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
       //Node top_q = Rewriter::rewrite( nn_e ).negate();
       Assert(top_q.getKind() == kind::FORALL);
       Trace("smt-qe") << "Get qe for " << top_q << std::endl;
-      ret_n = d_theoryEngine->getInstantiatedConjunction( top_q );
+      ret_n = te->getInstantiatedConjunction(top_q);
       Trace("smt-qe") << "Returned : " << ret_n << std::endl;
       if (n_e.getKind() == kind::EXISTS)
       {
@@ -2495,45 +2373,43 @@ bool SmtEngine::getAbduct(const Node& conj, Node& abd)
 
 void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
   SmtScope smts(this);
-  if( d_theoryEngine ){
-    std::vector< Node > qs_n;
-    d_theoryEngine->getInstantiatedQuantifiedFormulas( qs_n );
-    for( unsigned i=0; i<qs_n.size(); i++ ){
-      qs.push_back( qs_n[i].toExpr() );
-    }
-  }else{
-    Assert(false);
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
+  std::vector<Node> qs_n;
+  te->getInstantiatedQuantifiedFormulas(qs_n);
+  for (std::size_t i = 0, n = qs_n.size(); i < n; i++)
+  {
+    qs.push_back(qs_n[i].toExpr());
   }
 }
 
 void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) {
   SmtScope smts(this);
-  if( d_theoryEngine ){
-    std::vector< Node > insts_n;
-    d_theoryEngine->getInstantiations( Node::fromExpr( q ), insts_n );
-    for( unsigned i=0; i<insts_n.size(); i++ ){
-      insts.push_back( insts_n[i].toExpr() );
-    }
-  }else{
-    Assert(false);
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
+  std::vector<Node> insts_n;
+  te->getInstantiations(Node::fromExpr(q), insts_n);
+  for (std::size_t i = 0, n = insts_n.size(); i < n; i++)
+  {
+    insts.push_back(insts_n[i].toExpr());
   }
 }
 
 void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) {
   SmtScope smts(this);
   Assert(options::trackInstLemmas());
-  if( d_theoryEngine ){
-    std::vector< std::vector< Node > > tvecs_n;
-    d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n );
-    for( unsigned i=0; i<tvecs_n.size(); i++ ){
-      std::vector< Expr > tvec;
-      for( unsigned j=0; j<tvecs_n[i].size(); j++ ){
-        tvec.push_back( tvecs_n[i][j].toExpr() );
-      }
-      tvecs.push_back( tvec );
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
+  std::vector<std::vector<Node>> tvecs_n;
+  te->getInstantiationTermVectors(Node::fromExpr(q), tvecs_n);
+  for (std::size_t i = 0, n = tvecs_n.size(); i < n; i++)
+  {
+    std::vector<Expr> tvec;
+    for (std::size_t j = 0, m = tvecs_n[i].size(); j < m; j++)
+    {
+      tvec.push_back(tvecs_n[i][j].toExpr());
     }
-  }else{
-    Assert(false);
+    tvecs.push_back(tvec);
   }
 }
 
@@ -2568,7 +2444,7 @@ void SmtEngine::push()
   finishInit();
   d_state->doPendingPops();
   Trace("smt") << "SMT push()" << endl;
-  processAssertionsInternal();
+  d_smtSolver->processAssertions(*d_asserts);
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << PushCommand();
   }
@@ -2635,14 +2511,7 @@ void SmtEngine::resetAssertions()
   // push the state to maintain global context around everything
   d_state->setup();
 
-  /* Create new PropEngine.
-   * First force destruction of referenced PropEngine to enforce that
-   * statistics are unregistered by the obsolete PropEngine object before
-   * registered again by the new PropEngine object */
-  d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(
-      getTheoryEngine(), getContext(), getUserContext(), getResourceManager()));
-  d_theoryEngine->setPropEngine(getPropEngine());
+  d_smtSolver->resetAssertions();
 }
 
 void SmtEngine::interrupt()
@@ -2651,8 +2520,7 @@ void SmtEngine::interrupt()
   {
     return;
   }
-  d_propEngine->interrupt();
-  d_theoryEngine->interrupt();
+  d_smtSolver->interrupt();
 }
 
 void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
@@ -2707,7 +2575,9 @@ void SmtEngine::setUserAttribute(const std::string& attr,
   {
     node_values.push_back( expr_values[i].getNode() );
   }
-  d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value);
+  TheoryEngine* te = getTheoryEngine();
+  Assert(te != nullptr);
+  te->setUserAttribute(attr, expr.getNode(), node_values, str_value);
 }
 
 void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 4df57accb..1c71e371e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -103,6 +103,7 @@ class SmtNodeManagerListener;
 class OptionsManager;
 class Preprocessor;
 /** Subsolvers */
+class SmtSolver;
 class AbductionSolver;
 /**
  * Representation of a defined function.  We keep these around in
@@ -149,6 +150,7 @@ class CVC4_PUBLIC SmtEngine
   friend class ::CVC4::smt::SmtEngineState;
   friend class ::CVC4::smt::SmtScope;
   friend class ::CVC4::smt::ProcessAssertions;
+  friend class ::CVC4::smt::SmtSolver;
   friend ProofManager* ::CVC4::smt::currentProofManager();
   friend class ::CVC4::LogicRequest;
   friend class ::CVC4::theory::TheoryModel;
@@ -908,10 +910,10 @@ class CVC4_PUBLIC SmtEngine
   context::Context* getContext();
 
   /** Get a pointer to the TheoryEngine owned by this SmtEngine. */
-  TheoryEngine* getTheoryEngine() { return d_theoryEngine.get(); }
+  TheoryEngine* getTheoryEngine();
 
   /** Get a pointer to the PropEngine owned by this SmtEngine. */
-  prop::PropEngine* getPropEngine() { return d_propEngine.get(); }
+  prop::PropEngine* getPropEngine();
 
   /** Get a pointer to the ProofManager owned by this SmtEngine. */
   ProofManager* getProofManager() { return d_proofManager.get(); };
@@ -989,12 +991,6 @@ class CVC4_PUBLIC SmtEngine
   void shutdown();
 
   /**
-   * Full check of consistency in current context.  Returns true iff
-   * consistent.
-   */
-  Result check();
-
-  /**
    * Quick check of consistency in current context: calls
    * processAssertionList() then look for inconsistency (based only on
    * that).
@@ -1050,14 +1046,6 @@ class CVC4_PUBLIC SmtEngine
   void setLogicInternal();
 
   /**
-   * Process the assertions that have been asserted. This moves the set of
-   * assertions that have been buffered into the smt::Assertions object,
-   * preprocesses them, pushes them into the SMT solver, and clears the
-   * buffer.
-   */
-  void processAssertionsInternal();
-
-  /**
    * Add to Model command.  This is used for recording a command
    * that should be reported during a get-model call.
    */
@@ -1066,13 +1054,12 @@ class CVC4_PUBLIC SmtEngine
                                 bool userVisible = true,
                                 const char* dumpTag = "declarations");
 
-  /* Check satisfiability (used to check satisfiability and entailment). */
-  Result checkSatisfiability(const Node& assumption,
-                             bool inUnsatCore,
-                             bool isEntailmentCheck);
-  Result checkSatisfiability(const std::vector<Node>& assumptions,
-                             bool inUnsatCore,
-                             bool isEntailmentCheck);
+  /*
+   * Check satisfiability (used to check satisfiability and entailment).
+   */
+  Result checkSatInternal(const std::vector<Node>& assumptions,
+                          bool inUnsatCore,
+                          bool isEntailmentCheck);
 
   /**
    * Check that all Expr in formals are of BOUND_VARIABLE kind, where func is
@@ -1125,10 +1112,8 @@ class CVC4_PUBLIC SmtEngine
   /** Node manager listener */
   std::unique_ptr<smt::SmtNodeManagerListener> d_snmListener;
 
-  /** The theory engine */
-  std::unique_ptr<TheoryEngine> d_theoryEngine;
-  /** The propositional engine */
-  std::unique_ptr<prop::PropEngine> d_propEngine;
+  /** The SMT solver */
+  std::unique_ptr<smt::SmtSolver> d_smtSolver;
 
   /** The proof manager */
   std::unique_ptr<ProofManager> d_proofManager;
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
new file mode 100644
index 000000000..e0837c7cf
--- /dev/null
+++ b/src/smt/smt_solver.cpp
@@ -0,0 +1,257 @@
+/*********************                                                        */
+/*! \file smt_solver.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for SMT queries in an SmtEngine.
+ **/
+
+#include "smt/smt_solver.h"
+
+#include "proof/theory_proof.h"
+#include "prop/prop_engine.h"
+#include "smt/assertions.h"
+#include "smt/preprocessor.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_state.h"
+#include "theory/theory_engine.h"
+#include "theory/theory_traits.h"
+
+namespace CVC4 {
+namespace smt {
+
+SmtSolver::SmtSolver(SmtEngine& smt,
+                     SmtEngineState& state,
+                     ResourceManager* rm,
+                     Preprocessor& pp,
+                     SmtEngineStatistics& stats)
+    : d_smt(smt),
+      d_state(state),
+      d_rm(rm),
+      d_pp(pp),
+      d_stats(stats),
+      d_theoryEngine(nullptr),
+      d_propEngine(nullptr)
+{
+}
+
+SmtSolver::~SmtSolver() {}
+
+void SmtSolver::finishInit(const LogicInfo& logicInfo)
+{
+  // We have mutual dependency here, so we add the prop engine to the theory
+  // engine later (it is non-essential there)
+  d_theoryEngine.reset(new TheoryEngine(d_smt.getContext(),
+                                        d_smt.getUserContext(),
+                                        d_rm,
+                                        d_pp.getTermFormulaRemover(),
+                                        logicInfo));
+
+  // Add the theories
+  for (theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST;
+       ++id)
+  {
+    theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id);
+    // register with proof engine if applicable
+#ifdef CVC4_PROOF
+    ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(
+        d_theoryEngine->theoryOf(id));
+#endif
+  }
+
+  Trace("smt-debug") << "Making prop engine..." << std::endl;
+  /* force destruction of referenced PropEngine to enforce that statistics
+   * are unregistered by the obsolete PropEngine object before registered
+   * again by the new PropEngine object */
+  d_propEngine.reset(nullptr);
+  d_propEngine.reset(new PropEngine(
+      d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm));
+
+  Trace("smt-debug") << "Setting up theory engine..." << std::endl;
+  d_theoryEngine->setPropEngine(getPropEngine());
+  Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
+  d_theoryEngine->finishInit();
+}
+
+void SmtSolver::resetAssertions()
+{
+  /* Create new PropEngine.
+   * First force destruction of referenced PropEngine to enforce that
+   * statistics are unregistered by the obsolete PropEngine object before
+   * registered again by the new PropEngine object */
+  d_propEngine.reset(nullptr);
+  d_propEngine.reset(new PropEngine(
+      d_theoryEngine.get(), d_smt.getContext(), d_smt.getUserContext(), d_rm));
+  d_theoryEngine->setPropEngine(getPropEngine());
+  // Notice that we do not reset TheoryEngine, nor does it require calling
+  // finishInit again. In particular, TheoryEngine::finishInit does not
+  // depend on knowing the associated PropEngine.
+}
+
+void SmtSolver::interrupt()
+{
+  if (d_propEngine != nullptr)
+  {
+    d_propEngine->interrupt();
+  }
+  if (d_theoryEngine != nullptr)
+  {
+    d_theoryEngine->interrupt();
+  }
+}
+
+void SmtSolver::shutdown()
+{
+  if (d_propEngine != nullptr)
+  {
+    d_propEngine->shutdown();
+  }
+  if (d_theoryEngine != nullptr)
+  {
+    d_theoryEngine->shutdown();
+  }
+}
+
+Result SmtSolver::checkSatisfiability(Assertions& as,
+                                      const std::vector<Node>& assumptions,
+                                      bool inUnsatCore,
+                                      bool isEntailmentCheck)
+{
+  // update the state to indicate we are about to run a check-sat
+  bool hasAssumptions = !assumptions.empty();
+  d_state.notifyCheckSat(hasAssumptions);
+
+  // then, initialize the assertions
+  as.initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
+
+  // make the check
+  Assert(d_smt.isFullyInited());
+
+  Trace("smt") << "SmtSolver::check()" << endl;
+
+  const std::string& filename = d_state.getFilename();
+  if (d_rm->out())
+  {
+    Result::UnknownExplanation why =
+        d_rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
+    return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
+  }
+  d_rm->beginCall();
+
+  // Make sure the prop layer has all of the assertions
+  Trace("smt") << "SmtSolver::check(): processing assertions" << endl;
+  processAssertions(as);
+  Trace("smt") << "SmtSolver::check(): done processing assertions" << endl;
+
+  TimerStat::CodeTimer solveTimer(d_stats.d_solveTime);
+
+  Chat() << "solving..." << endl;
+  Trace("smt") << "SmtSolver::check(): running check" << endl;
+  Result result = d_propEngine->checkSat();
+
+  d_rm->endCall();
+  Trace("limit") << "SmtSolver::check(): cumulative millis "
+                 << d_rm->getTimeUsage() << ", resources "
+                 << d_rm->getResourceUsage() << endl;
+
+  if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
+      && result.asSatisfiabilityResult().isSat() == Result::UNSAT)
+  {
+    result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+  }
+  // flipped if we did a global negation
+  if (as.isGlobalNegated())
+  {
+    Trace("smt") << "SmtSolver::process global negate " << result << std::endl;
+    if (result.asSatisfiabilityResult().isSat() == Result::UNSAT)
+    {
+      result = Result(Result::SAT);
+    }
+    else if (result.asSatisfiabilityResult().isSat() == Result::SAT)
+    {
+      // Only can answer unsat if the theory is satisfaction complete. This
+      // includes linear arithmetic and bitvectors, which are the primary
+      // targets for the global negate option. Other logics are possible here
+      // but not considered.
+      LogicInfo logic = d_smt.getLogicInfo();
+      if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear()) ||
+          logic.isPure(theory::THEORY_BV))
+      {
+        result = Result(Result::UNSAT);
+      }
+      else
+      {
+        result = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+      }
+    }
+    Trace("smt") << "SmtSolver::global negate returned " << result << std::endl;
+  }
+
+  // set the filename on the result
+  Result r = Result(result, filename);
+  
+  // notify our state of the check-sat result
+  d_state.notifyCheckSatResult(hasAssumptions, r);
+
+  return r;
+}
+
+void SmtSolver::processAssertions(Assertions& as)
+{
+  TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime);
+  d_rm->spendResource(ResourceManager::Resource::PreprocessStep);
+  Assert(d_state.isFullyReady());
+
+  preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
+
+  if (ap.size() == 0)
+  {
+    // nothing to do
+    return;
+  }
+
+  // process the assertions with the preprocessor
+  bool noConflict = d_pp.process(as);
+
+  // notify theory engine new preprocessed assertions
+  d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
+
+  // Push the formula to decision engine
+  if (noConflict)
+  {
+    Chat() << "pushing to decision engine..." << endl;
+    d_propEngine->addAssertionsToDecisionEngine(ap);
+  }
+
+  // end: INVARIANT to maintain: no reordering of assertions or
+  // introducing new ones
+
+  d_pp.postprocess(as);
+
+  // Push the formula to SAT
+  {
+    Chat() << "converting to CNF..." << endl;
+    TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime);
+    for (const Node& assertion : ap.ref())
+    {
+      Chat() << "+ " << assertion << std::endl;
+      d_propEngine->assertFormula(assertion);
+    }
+  }
+
+  // clear the current assertions
+  as.clearCurrent();
+}
+
+TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
+
+prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
new file mode 100644
index 000000000..8d0644800
--- /dev/null
+++ b/src/smt/smt_solver.h
@@ -0,0 +1,137 @@
+/*********************                                                        */
+/*! \file smt_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for SMT queries in an SmtEngine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__SMT_SOLVER_H
+#define CVC4__SMT__SMT_SOLVER_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/logic_info.h"
+#include "util/result.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+class TheoryEngine;
+class ResourceManager;
+
+namespace prop {
+class PropEngine;
+}
+
+namespace smt {
+
+class Assertions;
+class SmtEngineState;
+class Preprocessor;
+class SmtEngineStatistics;
+
+/**
+ * A solver for SMT queries.
+ *
+ * This class manages the initialization of the theory engine and propositional
+ * engines and implements the method for checking satisfiability of the current
+ * set of assertions.
+ *
+ * Notice that this class is only conceptually responsible for running
+ * check-sat commands and an interface for sending formulas to the underlying
+ * classes. It does not implement any query techniques beyond getting the result
+ * (unsat/sat/unknown) of check-sat calls. More detailed information (e.g.
+ * models) can be queries using other classes that examine the state of the
+ * TheoryEngine directly, which can be accessed via getTheoryEngine.
+ */
+class SmtSolver
+{
+ public:
+  SmtSolver(SmtEngine& smt,
+            SmtEngineState& state,
+            ResourceManager* rm,
+            Preprocessor& pp,
+            SmtEngineStatistics& stats);
+  ~SmtSolver();
+  /**
+   * Create theory engine, prop engine based on the logic info.
+   */
+  void finishInit(const LogicInfo& logicInfo);
+  /** Reset all assertions, global declarations, etc.  */
+  void resetAssertions();
+  /**
+   * Interrupt a running query.  This can be called from another thread
+   * or from a signal handler.  Throws a ModalException if the SmtSolver
+   * isn't currently in a query.
+   */
+  void interrupt();
+  /**
+   * This is called by the destructor of SmtEngine, just before destroying the
+   * PropEngine, TheoryEngine, and DecisionEngine (in that order).  It
+   * is important because there are destruction ordering issues
+   * between PropEngine and Theory.
+   */
+  void shutdown();
+  /**
+   * Check satisfiability (used to check satisfiability and entailment)
+   * in SmtEngine. This is done via adding assumptions (when necessary) to
+   * assertions as, preprocessing and pushing assertions into the prop engine
+   * of this class, and checking for satisfiability via the prop engine.
+   *
+   * @param as The object managing the assertions in SmtEngine. This class
+   * maintains a current set of (unprocessed) assertions which are pushed
+   * into the internal members of this class (TheoryEngine and PropEngine)
+   * during this call.
+   * @param assumptions The assumptions for this check-sat call, which are
+   * temporary assertions.
+   * @param inUnsatCore Whether assumptions are in the unsat core.
+   * @param isEntailmentCheck Whether this is an entailment check (assumptions
+   * are negated in this case).
+   */
+  Result checkSatisfiability(Assertions& as,
+                             const std::vector<Node>& assumptions,
+                             bool inUnsatCore,
+                             bool isEntailmentCheck);
+  /**
+   * Process the assertions that have been asserted in as. This moves the set of
+   * assertions that have been buffered into as, preprocesses them, pushes them
+   * into the SMT solver, and clears the buffer.
+   */
+  void processAssertions(Assertions& as);
+  //------------------------------------------ access methods
+  /** Get a pointer to the TheoryEngine owned by this solver. */
+  TheoryEngine* getTheoryEngine();
+  /** Get a pointer to the PropEngine owned by this solver. */
+  prop::PropEngine* getPropEngine();
+  //------------------------------------------ end access methods
+ private:
+  /** Reference to the parent SMT engine */
+  SmtEngine& d_smt;
+  /** Reference to the state of the SmtEngine */
+  SmtEngineState& d_state;
+  /** Pointer to a resource manager (owned by SmtEngine) */
+  ResourceManager* d_rm;
+  /** Reference to the preprocessor of SmtEngine */
+  Preprocessor& d_pp;
+  /** Reference to the statistics of SmtEngine */
+  SmtEngineStatistics& d_stats;
+  /** The theory engine */
+  std::unique_ptr<TheoryEngine> d_theoryEngine;
+  /** The propositional engine */
+  std::unique_ptr<prop::PropEngine> d_propEngine;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__SMT_SOLVER_H */
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index dd0be5550..03b1922bd 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -114,10 +114,10 @@ public:
     // the following call, which constructs its underlying theory engine.
     d_smt->finishInit();
 
-    d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]->setOutputChannel(
+    d_smt->getTheoryEngine()->d_theoryTable[THEORY_ARITH]->setOutputChannel(
         d_outputChannel);
     d_arith = static_cast<TheoryArith*>(
-        d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]);
+        d_smt->getTheoryEngine()->d_theoryTable[THEORY_ARITH]);
 
     preregistered = new std::set<Node>();
 
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index ff1ce31b6..582a031c9 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -78,7 +78,7 @@ public:
     d_smt->finishInit();
     EagerBitblaster* bb = new EagerBitblaster(
         dynamic_cast<TheoryBV*>(
-            d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]),
+            d_smt->getTheoryEngine()->d_theoryTable[THEORY_BV]),
         d_smt->getContext());
     Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(16));
     Node y = d_nm->mkVar("y", d_nm->mkBitVectorType(16));
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 5da5a7c62..9693000a3 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -182,10 +182,10 @@ class TheoryBlack : public CxxTest::TestSuite {
     // the following call, which constructs its underlying theory engine.
     d_smt->finishInit();
     // guard against duplicate statistics assertion errors
-    delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN];
-    delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN];
-    d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL;
-    d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL;
+    delete d_smt->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN];
+    delete d_smt->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN];
+    d_smt->getTheoryEngine()->d_theoryTable[THEORY_BUILTIN] = NULL;
+    d_smt->getTheoryEngine()->d_theoryOut[THEORY_BUILTIN] = NULL;
 
     d_dummy = new DummyTheory(d_ctxt,
                               d_uctxt,