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

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

diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp
index 5975d3dd8c2c78404e2aa08f38599eb6f878db6c..c868ed2061cf766e71a8312ec33a3f45482263cd 100644 (file)
--- a/src/theory/shared_solver_distributed.cpp
+++ b/src/theory/shared_solver_distributed.cpp
@@ -19,8 +19,9 @@
 namespace CVC4 {
 namespace theory {
 
-SharedSolverDistributed::SharedSolverDistributed(TheoryEngine& te)
-    : SharedSolver(te)
+SharedSolverDistributed::SharedSolverDistributed(TheoryEngine& te,
+                                                 ProofNodeManager* pnm)
+    : SharedSolver(te, pnm)
 {
 }
 
@@ -67,7 +68,7 @@ TrustNode SharedSolverDistributed::explain(TNode literal, TheoryId id)
   TrustNode texp;
   if (id == THEORY_BUILTIN)
   {
-    // explanation based on the specific solver
+    // explanation using the shared terms database
     texp = d_sharedTerms.explain(literal);
     Trace("shared-solver")
         << "\tTerm was propagated by THEORY_BUILTIN. Explanation: "