8 files changed, 29 insertions, 28 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index d7514d50c..522427c03 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -13,6 +13,8 @@
  ** Node attributes.
  **/
 
+#include "cvc4_private.h"
+
 /* There are strong constraints on ordering of declarations of
  * attributes and nodes due to template use */
 #include "expr/node.h"
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 993bf3483..232a903e9 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -40,12 +40,12 @@ ExprManager::~ExprManager() {
 
 const BooleanType* ExprManager::booleanType() const {
   NodeManagerScope nms(d_nodeManager);
-  d_nodeManager->booleanType();
+  return d_nodeManager->booleanType();
 }
 
 const KindType* ExprManager::kindType() const {
   NodeManagerScope nms(d_nodeManager);
-  d_nodeManager->kindType();
+  return d_nodeManager->kindType();
 }
 
 Expr ExprManager::mkExpr(Kind kind) {
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 3ea1b581a..67fa0664a 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -18,7 +18,6 @@
 
 #include "cvc4_config.h"
 #include "expr/kind.h"
-#include "expr/node_manager.h"
 #include <vector>
 
 namespace CVC4 {
@@ -29,6 +28,7 @@ class BooleanType;
 class FunctionType; 
 class KindType;
 class SmtEngine;
+class NodeManager;
 
 class CVC4_PUBLIC ExprManager {
 
@@ -126,24 +126,5 @@ private:
 
 }/* CVC4 namespace */
 
-#include "expr/expr.h"
-
-namespace CVC4 {
-
-/**
- * A wrapper (essentially) for NodeManagerScope.  Without this, we'd
- * need Expr to be a friend of ExprManager.
- */
-class ExprManagerScope {
-  NodeManagerScope d_nms;
-public:
-  inline ExprManagerScope(const Expr& e) :
-    d_nms(e.getExprManager() == NULL ?
-          NodeManager::currentNM() : e.getExprManager()->getNodeManager()) {
-  }
-};
-
-}/* CVC4 namespace */
-
 #endif /* __CVC4__EXPR_MANAGER_H */
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 25f0b7453..fe2016747 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -13,6 +13,8 @@
  ** Reference-counted encapsulation of a pointer to node information.
  **/
 
+#include "cvc4_private.h"
+
 #include "expr/node_value.h"
 
 #ifndef __CVC4__NODE_H
@@ -690,12 +692,12 @@ template<bool ref_count>
  * to find the symbol, and use it, which is the first standard this code needs
  * to meet. A cleaner solution is welcomed.
  */
-static void CVC4_PUBLIC debugPrintNode(const NodeTemplate<true>& n) {
+static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) {
   n.printAst(Warning(), 0);
   Warning().flush();
 }
 
-static void CVC4_PUBLIC debugPrintTNode(const NodeTemplate<false>& n) {
+static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) {
   n.printAst(Warning(), 0);
   Warning().flush();
 }
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 03936c89a..c1b2a87d2 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -13,6 +13,8 @@
  ** A builder interface for nodes.
  **/
 
+#include "cvc4_private.h"
+
 /* strong dependency; make sure node is included first */
 #include "node.h"
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 9d2b0947e..00fcf52c4 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -13,6 +13,8 @@
  ** A manager for Nodes.
  **/
 
+#include "cvc4_private.h"
+
 /* circular dependency; force node.h first */
 #include "expr/attribute.h"
 #include "expr/node.h"
@@ -25,6 +27,7 @@
 #include <ext/hash_set>
 
 #include "expr/kind.h"
+#include "expr/expr.h"
 
 namespace __gnu_cxx {
   template<>
@@ -155,6 +158,19 @@ public:
   }
 };
 
+/**
+ * A wrapper (essentially) for NodeManagerScope.  Without this, we'd
+ * need Expr to be a friend of ExprManager.
+ */
+class ExprManagerScope {
+  NodeManagerScope d_nms;
+public:
+  inline ExprManagerScope(const Expr& e) :
+    d_nms(e.getExprManager() == NULL ?
+          NodeManager::currentNM() : e.getExprManager()->getNodeManager()) {
+  }
+};
+
 template <class AttrKind>
 inline typename AttrKind::value_type NodeManager::getAttribute(TNode n,
                                                                const AttrKind&) const {
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 85b8a6d60..e8435df26 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -17,9 +17,7 @@
  ** reference count on NodeValue instances and
  **/
 
-/* this must be above the check for __CVC4__EXPR__NODE_VALUE_H */
-/* to resolve a circular dependency */
-//#include "expr/node.h"
+#include "cvc4_private.h"
 
 #ifndef __CVC4__EXPR__NODE_VALUE_H
 #define __CVC4__EXPR__NODE_VALUE_H
diff --git a/src/expr/type.h b/src/expr/type.h
index 77994eec5..7009ed504 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -28,7 +28,7 @@ class NodeManager;
 /**
  * Class encapsulating CVC4 expression types.
  */
-class Type {
+class CVC4_PUBLIC Type {
 public:
   /** Comparision for equality */
   bool operator==(const Type& t) const;