Fix

4 files changed, 9 insertions, 3 deletions

diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index 64bebcfe4..a351672b8 100644
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -62,4 +62,9 @@ std::shared_ptr<ProofNode> PRefProofGenerator::getProofFor(Node f)
   return d_proof->mkProof(f);
 }
 
+std::string PRefProofGenerator::identify() const
+{
+  return "PRefProofGenerator";
+}
+
 }  // namespace CVC4
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 88a989e87..0546aac52 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -75,11 +75,12 @@ class CDProof;
 class PRefProofGenerator : public ProofGenerator
 {
  public:
-  PRefProofGenerator(CDProof* cd);
+  PRefProofGenerator(std::string name, CDProof* cd);
   ~PRefProofGenerator();
   /** Get proof for */
   std::shared_ptr<ProofNode> getProofFor(Node f) override;
-
+  /** Identify this generator (for debugging, etc..) */
+  std::string identify() const override;
  protected:
   /** The reference proof */
   CDProof* d_proof;
diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp
index c54f56de7..43f8a1b8e 100644
--- a/src/theory/trust_node.cpp
+++ b/src/theory/trust_node.cpp
@@ -15,6 +15,7 @@
 #include "theory/trust_node.h"
 
 #include "theory/proof_engine_output_channel.h"
+#include "expr/proof_generator.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h
index b1bd12859..991a5dac2 100644
--- a/src/theory/trust_node.h
+++ b/src/theory/trust_node.h
@@ -18,7 +18,6 @@
 #define CVC4__THEORY__TRUST_NODE_H
 
 #include "expr/node.h"
-#include "expr/proof_generator.h"
 
 namespace CVC4 {