[proof-new] Connecting new unsat cores (#5834)

Allows one to generate unsat cores from the new proof infrastructure. For new this is controlled by a new option, --check-unsat-cores-new.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a1fc809e4..eb8eb6ca0 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -118,6 +118,7 @@ struct SmtEngineStatistics;
 class SmtScope;
 class ProcessAssertions;
 class PfManager;
+class UnsatCoreManager;
 
 ProofManager* currentProofManager();
 }/* CVC4::smt namespace */
@@ -1101,6 +1102,11 @@ class CVC4_PUBLIC SmtEngine
   std::unique_ptr<smt::PfManager> d_pfManager;
 
   /**
+   * The unsat core manager, which produces unsat cores and related information
+   * from refutations. */
+  std::unique_ptr<smt::UnsatCoreManager> d_ucManager;
+
+  /**
    * The rewriter associated with this SmtEngine. We have a different instance
    * of the rewriter for each SmtEngine instance. This is because rewriters may
    * hold references to objects that belong to theory solvers, which are