From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 28 Apr 2015 01:11:29 +0000 (-0700)
Subject: Fixed problem with private/public header clash
X-Git-Tag: cvc5-1.0.0~6337^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=721cbfad7ebe3668e87679f65e7ce80251878dc6;p=cvc5.git

Fixed problem with private/public header clash
---

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() {}