X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Ftheory%2Fshared_solver_distributed.cpp;h=c868ed2061cf766e71a8312ec33a3f45482263cd;hb=26601663d6cc8fb8613df5a1d253eba8743e57cb;hp=5975d3dd8c2c78404e2aa08f38599eb6f878db6c;hpb=7f396917c481de7a57782a5daf31992c37d7d964;p=cvc5.git

diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp
index 5975d3dd8..c868ed206 100644
--- 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: "