Added option for --check-unsat-cores and various core bug fixes (merge of Morgan's proof branch).

1 files changed, 12 insertions, 0 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 7c5c45e42..de9b8127d 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -186,6 +186,13 @@ class CVC4_PUBLIC SmtEngine {
   std::vector<Command*> d_dumpCommands;
 
   /**
+   *A vector of command definitions to be imported in the new
+   *SmtEngine when checking unsat-cores.
+   */
+#ifdef CVC4_PROOF  
+  std::vector<Command*> d_defineCommands;
+#endif   
+  /**
    * The logic we're in.
    */
   LogicInfo d_logic;
@@ -261,6 +268,11 @@ class CVC4_PUBLIC SmtEngine {
   void checkProof();
 
   /**
+   * Check that an unsatisfiable core is indeed unsatisfiable.
+   */
+  void checkUnsatCore();
+
+  /**
    * Check that a generated Model (via getModel()) actually satisfies
    * all user assertions.
    */