1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 99c80dd4a..2f882e257 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__BOOLEANS__THEORY_BOOL_H
 
 #include "context/context.h"
+#include "theory/booleans/proof_checker.h"
 #include "theory/booleans/theory_bool_rewriter.h"
 #include "theory/theory.h"
 
@@ -33,19 +34,20 @@ class TheoryBool : public Theory {
              context::UserContext* u,
              OutputChannel& out,
              Valuation valuation,
-             const LogicInfo& logicInfo);
+             const LogicInfo& logicInfo,
+             ProofNodeManager* pnm = nullptr);
 
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
-  //void check(Effort);
-
   std::string identify() const override { return std::string("TheoryBool"); }
 
  private:
   /** The theory rewriter for this theory. */
   TheoryBoolRewriter d_rewriter;
+  /** Proof rule checker */
+  BoolProofRuleChecker d_bProofChecker;
 };/* class TheoryBool */
 
 }/* CVC4::theory::booleans namespace */