From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 8 Apr 2020 13:50:14 +0000 (-0500)
Subject: Eliminate call to currentNM within NodeManager (#4227)
X-Git-Tag: cvc5-1.0.0~3397
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=98a78889a4c4168f9c6632a0e19e1b8f422c4a9d;p=cvc5.git

Eliminate call to currentNM within NodeManager (#4227)

Eliminates 2 unintentional calls to the global access function.
---

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 16ffd8306..efac34902 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -754,9 +754,9 @@ Node NodeManager::getBoundVarListForFunctionType( TypeNode tn ) {
   if( bvl.isNull() ){
     std::vector< Node > vars;
     for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
-      vars.push_back( NodeManager::currentNM()->mkBoundVar( tn[i] ) );
+      vars.push_back(mkBoundVar(tn[i]));
     }
-    bvl = NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, vars );
+    bvl = mkNode(kind::BOUND_VAR_LIST, vars);
     Trace("functions") << "Make standard bound var list " << bvl << " for " << tn << std::endl;
     tn.setAttribute(LambdaBoundVarListAttr(),bvl);
   }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 2e8f40fff..aea49d979 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -517,7 +517,7 @@ public:
   Node* mkBoundVarPtr(const TypeNode& type);
 
   /** get the canonical bound variable list for function type tn */
-  static Node getBoundVarListForFunctionType( TypeNode tn );
+  Node getBoundVarListForFunctionType( TypeNode tn );
 
   /**
    * Optional flags used to control behavior of NodeManager::mkSkolem().