From: Tim King <taking@google.com>
Date: Thu, 16 Mar 2017 21:06:17 +0000 (-0700)
Subject: Fixes bug 781. Copy constructor for Expr needed to set the NodeManagerScope.
X-Git-Tag: cvc5-1.0.0~5884
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=afe84522b87b6fc0ad5d0e9a396b61f7b523f674;p=cvc5.git

Fixes bug 781. Copy constructor for Expr needed to set the NodeManagerScope.
---

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index dad437bc6..4fbb0cd33 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -82,16 +82,22 @@ Expr TypeCheckingException::getExpression() const throw() {
 Expr::Expr() :
   d_node(new Node),
   d_exprManager(NULL) {
+  // We do not need to wrap this in an ExprManagerScope as `new Node` is backed
+  // by NodeValue::null which is a static outside of a NodeManager.
 }
 
 Expr::Expr(ExprManager* em, Node* node) :
   d_node(node),
   d_exprManager(em) {
+  // We do not need to wrap this in an ExprManagerScope as this only initializes
+  // pointers
 }
 
 Expr::Expr(const Expr& e) :
-  d_node(new Node(*e.d_node)),
+  d_node(NULL),
   d_exprManager(e.d_exprManager) {
+  ExprManagerScope ems(*this);
+  d_node = new Node(*e.d_node);
 }
 
 Expr::~Expr() {
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 5f62317ee..6ce7b0a18 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -37,24 +37,25 @@ Type Type::makeType(const TypeNode& typeNode) const {
   return Type(d_nodeManager, new TypeNode(typeNode));
 }
 
-Type::Type(NodeManager* nm, TypeNode* node) :
-  d_typeNode(node),
-  d_nodeManager(nm) {
+Type::Type(NodeManager* nm, TypeNode* node)
+    : d_typeNode(node), d_nodeManager(nm) {
+  // This does not require a NodeManagerScope as this is restricted to be an
+  // internal only pointer initialization call.
 }
 
-Type::~Type() {
-  NodeManagerScope nms(d_nodeManager);
-  delete d_typeNode;
+Type::Type() : d_typeNode(new TypeNode), d_nodeManager(NULL) {
+  // This does not require a NodeManagerScope as `new TypeNode` is backed by a
+  // static expr::NodeValue::null().
 }
 
-Type::Type() :
-  d_typeNode(new TypeNode),
-  d_nodeManager(NULL) {
+Type::Type(const Type& t) : d_typeNode(NULL), d_nodeManager(t.d_nodeManager) {
+  NodeManagerScope nms(d_nodeManager);
+  d_typeNode = new TypeNode(*t.d_typeNode);
 }
 
-Type::Type(const Type& t) :
-  d_typeNode(new TypeNode(*t.d_typeNode)),
-  d_nodeManager(t.d_nodeManager) {
+Type::~Type() {
+  NodeManagerScope nms(d_nodeManager);
+  delete d_typeNode;
 }
 
 bool Type::isNull() const {