1 files changed, 27 insertions, 0 deletions
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 35f94194f..298f9b4c6 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -105,6 +105,33 @@ class ProofGenerator
   virtual std::string identify() const = 0;
 };
 
+/**
+ * Debug check closed on Trace c. Context ctx is string for debugging.
+ * This method throws an assertion failure if pg cannot provide a closed
+ * proof for fact proven. This is checked only if --proof-new-eager-checking
+ * is enabled or the Trace c is enabled.
+ *
+ * @param reqGen Whether we consider a null generator to be a failure.
+ */
+void pfgEnsureClosed(Node proven,
+                     ProofGenerator* pg,
+                     const char* c,
+                     const char* ctx,
+                     bool reqGen = true);
+
+/**
+ * Debug check closed with Trace c. Context ctx is string for debugging and
+ * assumps is the set of allowed open assertions.
+ *
+ * @param reqGen Whether we consider a null generator to be a failure.
+ */
+void pfgEnsureClosedWrt(Node proven,
+                        ProofGenerator* pg,
+                        const std::vector<Node>& assumps,
+                        const char* c,
+                        const char* ctx,
+                        bool reqGen = true);
+
 }  // namespace CVC4
 
 #endif /* CVC4__EXPR__PROOF_GENERATOR_H */