Fixed problem with private/public header clash

diff --git a/src/util/unsat_core.cpp b/src/util/unsat_core.cpp
index 929d5e909c737ea851e703eb916587cd2f15cc24..95d066c6dffad6094dd2b27d21dad574abb6e521 100644 (file)
--- 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 8f497688ae5c1d77a4f2e6cea6b9e8ecacf2970a..644f56509d8be4bd3d3701c922877acb181a6aa2 100644 (file)
--- 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() {}