1 files changed, 11 insertions, 4 deletions
diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h
index a19903f12..d8fae8a55 100644
--- a/src/proof/alethe/alethe_post_processor.h
+++ b/src/proof/alethe/alethe_post_processor.h
@@ -16,8 +16,9 @@
 #ifndef CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H
 #define CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H
 
-#include "proof/alethe/alethe_proof_rule.h"
 #include "proof/proof_node_updater.h"
+#include "proof/alethe/alethe_node_converter.h"
+#include "proof/alethe/alethe_proof_rule.h"
 
 namespace cvc5 {
 
@@ -30,7 +31,8 @@ namespace proof {
 class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
 {
  public:
-  AletheProofPostprocessCallback(ProofNodeManager* pnm);
+  AletheProofPostprocessCallback(ProofNodeManager* pnm,
+                                 AletheNodeConverter& anc);
   ~AletheProofPostprocessCallback() {}
   /** Should proof pn be updated? Only if its top-level proof rule is not an
    *  Alethe proof rule.
@@ -52,6 +54,8 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
  private:
   /** The proof node manager */
   ProofNodeManager* d_pnm;
+  /** The Alethe node converter */
+  AletheNodeConverter& d_anc;
   /** The cl operator
    * For every step the conclusion is a clause. But since the or operator
    *requires at least two arguments it is extended by the cl operator. In case
@@ -114,7 +118,8 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
 class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 {
  public:
-  AletheProofPostprocessFinalCallback(ProofNodeManager* pnm);
+   AletheProofPostprocessFinalCallback(ProofNodeManager* pnm,
+                                       AletheNodeConverter& anc);
   ~AletheProofPostprocessFinalCallback() {}
   /** Should proof pn be updated? It should, if the last step is printed as (cl
    * false) or if it is an assumption (in that case it is printed as false).
@@ -139,6 +144,8 @@ class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
  private:
   /** The proof node manager */
   ProofNodeManager* d_pnm;
+  /** The Alethe node converter */
+  AletheNodeConverter& d_anc;
   /** The cl operator is defined as described in the
    * AletheProofPostprocessCallback class above
    **/
@@ -152,7 +159,7 @@ class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
 class AletheProofPostprocess
 {
  public:
-  AletheProofPostprocess(ProofNodeManager* pnm);
+   AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc);
   ~AletheProofPostprocess();
   /** post-process */
   void process(std::shared_ptr<ProofNode> pf);