1 files changed, 13 insertions, 0 deletions
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a0496a525..6812a6549 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -286,6 +286,13 @@ class PropEngine
 
   /** Is proof enabled? */
   bool isProofEnabled() const;
+
+  /** Retrieve unsat core from SAT solver for assumption-based unsat cores. */
+  void getUnsatCore(std::vector<Node>& core);
+
+  /** Return the prop engine proof for assumption-based unsat cores. */
+  std::shared_ptr<ProofNode> getRefutation();
+
  private:
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
@@ -370,6 +377,12 @@ class PropEngine
 
   /** Reference to the output manager of the smt engine */
   OutputManager& d_outMgr;
+
+  /**
+   * Stores assumptions added via assertInternal() if assumption-based unsat
+   * cores are enabled.
+   */
+  context::CDList<Node> d_assumptions;
 };
 
 }  // namespace prop