1 files changed, 20 insertions, 2 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 13960b717..e52776fce 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -23,9 +23,11 @@
 #include <utility>
 
 #include "base/cvc4_assert.h"
+#include "base/listener.h"
 #include "base/tls.h"
 #include "expr/attribute.h"
 #include "expr/node_manager_attributes.h"
+#include "expr/node_manager_listeners.h"
 #include "expr/type_checker.h"
 #include "options/options.h"
 #include "options/smt_options.h"
@@ -84,6 +86,7 @@ NodeManager::NodeManager(ExprManager* exprManager) :
   d_options(new Options()),
   d_statisticsRegistry(new StatisticsRegistry()),
   d_resourceManager(new ResourceManager()),
+  d_registrations(new ListenerRegistrationList()),
   next_id(0),
   d_attrManager(new expr::attr::AttributeManager()),
   d_exprManager(exprManager),
@@ -96,16 +99,19 @@ NodeManager::NodeManager(ExprManager* exprManager) :
 
 NodeManager::NodeManager(ExprManager* exprManager,
                          const Options& options) :
-  d_options(new Options(options)),
+  d_options(new Options()),
   d_statisticsRegistry(new StatisticsRegistry()),
   d_resourceManager(new ResourceManager()),
+  d_registrations(new ListenerRegistrationList()),
   next_id(0),
   d_attrManager(new expr::attr::AttributeManager()),
   d_exprManager(exprManager),
   d_nodeUnderDeletion(NULL),
   d_inReclaimZombies(false),
   d_abstractValueCount(0),
-  d_skolemCounter(0) {
+  d_skolemCounter(0)
+{
+  d_options->copyValues(options);
   init();
 }
 
@@ -135,6 +141,16 @@ void NodeManager::init() {
   if((*d_options)[options::cpuTime]) {
     d_resourceManager->useCPUTime(true);
   }
+
+  // Do not notify() upon registration as these were handled manually above.
+  d_registrations->add(d_options->registerTlimitListener(
+      new TlimitListener(d_resourceManager), false));
+  d_registrations->add(d_options->registerTlimitPerListener(
+      new TlimitPerListener(d_resourceManager), false));
+  d_registrations->add(d_options->registerRlimitListener(
+      new RlimitListener(d_resourceManager), false));
+  d_registrations->add(d_options->registerRlimitPerListener(
+      new RlimitPerListener(d_resourceManager), false));
 }
 
 NodeManager::~NodeManager() {
@@ -180,6 +196,8 @@ NodeManager::~NodeManager() {
   // defensive coding, in case destruction-order issues pop up (they often do)
   delete d_statisticsRegistry;
   d_statisticsRegistry = NULL;
+  delete d_registrations;
+  d_registrations = NULL;
   delete d_resourceManager;
   d_resourceManager = NULL;
   delete d_attrManager;