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

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

diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp
index 794d3ca7c49789eb9d07012816efd417aebc428e..24d7d29cfe66e81d1f1138ecdcf9cd322c19b2b1 100644 (file)
--- a/src/theory/shared_solver.cpp
+++ b/src/theory/shared_solver.cpp
@@ -26,10 +26,10 @@ namespace theory {
 // In distributed equality engine management, shared terms database also
 // maintains an equality engine. In central equality engine management,
 // it does not.
-SharedSolver::SharedSolver(TheoryEngine& te)
+SharedSolver::SharedSolver(TheoryEngine& te, ProofNodeManager* pnm)
     : d_te(te),
       d_logicInfo(te.getLogicInfo()),
-      d_sharedTerms(&d_te, d_te.getSatContext()),
+      d_sharedTerms(&d_te, d_te.getSatContext(), d_te.getUserContext(), pnm),
       d_sharedTermsVisitor(d_sharedTerms)
 {
 }