1 files changed, 11 insertions, 0 deletions
diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 8d0644800..07d81f92b 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -28,6 +28,7 @@ namespace CVC4 {
 class SmtEngine;
 class TheoryEngine;
 class ResourceManager;
+class ProofNodeManager;
 
 namespace prop {
 class PropEngine;
@@ -108,6 +109,11 @@ class SmtSolver
    * into the SMT solver, and clears the buffer.
    */
   void processAssertions(Assertions& as);
+  /**
+   * Set proof node manager. Enables proofs in this SmtSolver. Should be
+   * called before finishInit.
+   */
+  void setProofNodeManager(ProofNodeManager* pnm);
   //------------------------------------------ access methods
   /** Get a pointer to the TheoryEngine owned by this solver. */
   TheoryEngine* getTheoryEngine();
@@ -125,6 +131,11 @@ class SmtSolver
   Preprocessor& d_pp;
   /** Reference to the statistics of SmtEngine */
   SmtEngineStatistics& d_stats;
+  /**
+   * Pointer to the proof node manager used by this SmtSolver. A non-null
+   * proof node manager indicates that proofs are enabled.
+   */
+  ProofNodeManager* d_pnm;
   /** The theory engine */
   std::unique_ptr<TheoryEngine> d_theoryEngine;
   /** The propositional engine */