Fixed problem with private/public header clash

2 files changed, 7 insertions, 2 deletions

diff --git a/src/util/unsat_core.cpp b/src/util/unsat_core.cpp
index 929d5e909..95d066c6d 100644
--- a/src/util/unsat_core.cpp
+++ b/src/util/unsat_core.cpp
@@ -21,6 +21,10 @@
 
 namespace CVC4 {
 
+void UnsatCore::initMessage() const {
+  Debug("core") << "UnsatCore size " << d_core.size() << std::endl;
+}
+
 UnsatCore::const_iterator UnsatCore::begin() const {
   return d_core.begin();
 }
diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h
index 8f497688a..644f56509 100644
--- a/src/util/unsat_core.h
+++ b/src/util/unsat_core.h
@@ -23,7 +23,6 @@
 #include <iostream>
 #include <vector>
 #include "expr/expr.h"
-#include "util/output.h"
 
 namespace CVC4 {
 
@@ -40,12 +39,14 @@ class CVC4_PUBLIC UnsatCore {
 
   std::vector<Expr> d_core;
 
+  void initMessage() const;
+
 public:
   UnsatCore() : d_smt(NULL) {}
 
   template <class T>
   UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {
-    Debug("core") << "UnsatCore size " << d_core.size() << std::endl;
+    initMessage();
   }
 
   ~UnsatCore() {}