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

1 files changed, 6 insertions, 1 deletions

diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h
index 27cf86488..8f497688a 100644
--- a/src/util/unsat_core.h
+++ b/src/util/unsat_core.h
@@ -23,6 +23,7 @@
 #include <iostream>
 #include <vector>
 #include "expr/expr.h"
+#include "util/output.h"
 
 namespace CVC4 {
 
@@ -43,13 +44,17 @@ public:
   UnsatCore() : d_smt(NULL) {}
 
   template <class T>
-  UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {}
+  UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {
+    Debug("core") << "UnsatCore size " << d_core.size() << std::endl;
+  }
 
   ~UnsatCore() {}
 
   /** get the smt engine that this unsat core is hooked up to */
   SmtEngine* getSmtEngine() { return d_smt; }
 
+  size_t size() const { return d_core.size(); }
+
   typedef std::vector<Expr>::const_iterator iterator;
   typedef std::vector<Expr>::const_iterator const_iterator;