1 files changed, 16 insertions, 0 deletions
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 {