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";
   }