1 files changed, 12 insertions, 0 deletions
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index e41df9593..3b6ba7069 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3741,6 +3741,18 @@ class CVC5_EXPORT Solver
   std::vector<Term> getUnsatCore() const;
 
   /**
+   * Get the refutation proof
+   * SMT-LIB:
+   * \verbatim
+   * ( get-proof )
+   * \endverbatim
+   * Requires to enable option 'produce-proofs'.
+   * @return a string representing the proof, according to the the value of
+   * proof-format-mode.
+   */
+  std::string getProof() const;
+
+  /**
    * Get the value of the given term.
    * SMT-LIB:
    * \verbatim