(proof-new) Make shared solver proof producing (#5169)

[cvc5.git] / src / theory / combination_engine.cpp

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index 32af150547356f324669554f16d0ef8df3628143..5e242659f238c350073e99dff8fc721b66f0888d 100644 (file)
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -28,6 +28,7 @@ CombinationEngine::CombinationEngine(TheoryEngine& te,
                                      const std::vector<Theory*>& paraTheories,
                                      ProofNodeManager* pnm)
     : d_te(te),
+      d_pnm(pnm),
       d_logicInfo(te.getLogicInfo()),
       d_paraTheories(paraTheories),
       d_eemanager(nullptr),
@@ -46,7 +47,7 @@ void CombinationEngine::finishInit()
   if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
   {
     // use the distributed shared solver
-    d_sharedSolver.reset(new SharedSolverDistributed(d_te));
+    d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm));
     // make the distributed equality engine manager
     d_eemanager.reset(
         new EqEngineManagerDistributed(d_te, *d_sharedSolver.get()));