diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f52c7732f..390af8967 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -32,11 +32,11 @@ #include <string> #include <ext/hash_set> +#include "base/tls.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" #include "util/subrange_bound.h" -#include "util/tls.h" #include "options/options.h" namespace CVC4 { @@ -940,24 +940,25 @@ public: class NodeManagerScope { /** The old NodeManager, to be restored on destruction. */ NodeManager* d_oldNodeManager; - + Options::OptionsScope d_optionsScope; public: - NodeManagerScope(NodeManager* nm) : - d_oldNodeManager(NodeManager::s_current) { + NodeManagerScope(NodeManager* nm) + : d_oldNodeManager(NodeManager::s_current) + , d_optionsScope(nm ? nm->d_options : NULL) { // There are corner cases where nm can be NULL and it's ok. // For example, if you write { Expr e; }, then when the null // Expr is destructed, there's no active node manager. //Assert(nm != NULL); NodeManager::s_current = nm; - Options::s_current = nm ? nm->d_options : NULL; + //Options::s_current = nm ? nm->d_options : NULL; Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } ~NodeManagerScope() { NodeManager::s_current = d_oldNodeManager; - Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL; + //Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL; Debug("current") << "node manager scope: " << "returning to " << NodeManager::s_current << "\n"; } |