1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 7b91191f9..03c733451 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -46,6 +46,7 @@ namespace cvc5 {
 class ResourceManager;
 class OutputManager;
 class TheoryEngineProofGenerator;
+class ProofChecker;
 
 /**
  * A pair of a theory and a node. This is used to mark the flow of
@@ -322,6 +323,9 @@ class TheoryEngine {
         theoryId, d_theoryTable[theoryId]->getTheoryRewriter());
   }
 
+  /** Register theory proof rule checkers to the given proof checker */
+  void initializeProofChecker(ProofChecker* pc);
+
   void setPropEngine(prop::PropEngine* propEngine)
   {
     d_propEngine = propEngine;