1 files changed, 10 insertions, 0 deletions
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 21644d3f4..2389181b5 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -22,10 +22,14 @@
 #include "util/cvc4_assert.h"
 #include "expr/node_manager.h"
 #include "util/output.h"
+#include "proof/proof.h"
 
 #pragma once
 
 namespace CVC4 {
+
+class ProofManager;
+
 namespace smt {
 
 extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
@@ -35,6 +39,12 @@ inline SmtEngine* currentSmtEngine() {
   return s_smtEngine_current;
 }
 
+inline ProofManager* currentProofManager() {
+  Assert(PROOF_ON());
+  Assert(s_smtEngine_current != NULL);
+  return s_smtEngine_current->d_proofManager;
+}
+
 class SmtScope : public NodeManagerScope {
   /** The old NodeManager, to be restored on destruction. */
   SmtEngine* d_oldSmtEngine;