Hack to support global variables for CVC language extended to export mechanism.

- Adds GlobalVarAttr node attribute

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 5 insertions, 2 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index ed643b830..a3204f00f 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -138,12 +138,15 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
       if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) {
         // temporarily set the node manager to NULL; this gets around
         // a check that mkVar isn't called internally
-        NodeManagerScope nullScope(NULL);
 
         if(n.getKind() == kind::BOUND_VAR_LIST || n.getKind() == kind::BOUND_VARIABLE) {
+          NodeManagerScope nullScope(NULL);
           to_e = to->mkBoundVar(name, type);// FIXME thread safety
         } else if(n.getKind() == kind::VARIABLE) {
-          to_e = to->mkVar(name, type);// FIXME thread safety
+          bool isGlobal;
+          Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal);
+          NodeManagerScope nullScope(NULL);
+          to_e = to->mkVar(name, type, isGlobal);// FIXME thread safety
         } else if(n.getKind() == kind::SKOLEM) {
           // skolems are only available at the Node level (not the Expr level)
           TypeNode typeNode = TypeNode::fromType(type);