1 files changed, 8 insertions, 8 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6c34eb4a3..501a0f4fd 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -41,7 +41,7 @@
 #include "util/subrange_bound.h"
 #include "util/configuration_private.h"
 #include "util/tls.h"
-#include "util/options.h"
+#include "options/options.h"
 
 namespace CVC4 {
 
@@ -83,7 +83,7 @@ class NodeManager {
 
   static CVC4_THREADLOCAL(NodeManager*) s_current;
 
-  Options d_options;
+  Options* d_options;
   StatisticsRegistry* d_statisticsRegistry;
 
   NodeValuePool d_nodeValuePool;
@@ -267,13 +267,13 @@ public:
   static NodeManager* currentNM() { return s_current; }
 
   /** Get this node manager's options (const version) */
-  const Options* getOptions() const {
-    return &d_options;
+  const Options& getOptions() const {
+    return *d_options;
   }
 
   /** Get this node manager's options (non-const version) */
-  Options* getOptions() {
-    return &d_options;
+  Options& getOptions() {
+    return *d_options;
   }
 
   /** Get this node manager's statistics registry */
@@ -791,14 +791,14 @@ public:
     // 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";
   }