Some defensive programming at destruction time, and fix a latent dangling pointer bug.

3 files changed, 18 insertions, 0 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 7ce51ecdd..8bcfd58ba 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -105,18 +105,22 @@ ExprManager::~ExprManager() throw() {
       if (d_exprStatistics[i] != NULL) {
         d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]);
         delete d_exprStatistics[i];
+        d_exprStatistics[i] = NULL;
       }
     }
     for (unsigned i = 0; i < LAST_TYPE; ++ i) {
       if (d_exprStatisticsVars[i] != NULL) {
         d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]);
         delete d_exprStatisticsVars[i];
+        d_exprStatisticsVars[i] = NULL;
       }
     }
 #endif
 
     delete d_nodeManager;
+    d_nodeManager = NULL;
     delete d_ctxt;
+    d_ctxt = NULL;
 
   } catch(Exception& e) {
     Warning() << "CVC4 threw an exception during cleanup." << std::endl
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index d0a477b9a..fb1284d0d 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -136,6 +136,8 @@ NodeManager::~NodeManager() {
     d_operators[i] = Node::null();
   }
 
+  d_tupleAndRecordTypes.clear();
+
   Assert(!d_attrManager->inGarbageCollection() );
   while(!d_zombies.empty()) {
     reclaimZombies();
@@ -157,9 +159,13 @@ NodeManager::~NodeManager() {
     Debug("gc:leaks") << ":end:" << endl;
   }
 
+  // defensive coding, in case destruction-order issues pop up (they often do)
   delete d_statisticsRegistry;
+  d_statisticsRegistry = NULL;
   delete d_attrManager;
+  d_attrManager = NULL;
   delete d_options;
+  d_options = NULL;
 }
 
 void NodeManager::reclaimZombies() {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2a12b07de..dcfc526ec 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -809,6 +809,7 @@ SmtEngine::~SmtEngine() throw() {
 
     for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
       delete d_dumpCommands[i];
+      d_dumpCommands[i] = NULL;
     }
     d_dumpCommands.clear();
 
@@ -819,15 +820,22 @@ SmtEngine::~SmtEngine() throw() {
     d_definedFunctions->deleteSelf();
 
     delete d_theoryEngine;
+    d_theoryEngine = NULL;
     delete d_propEngine;
+    d_propEngine = NULL;
     delete d_decisionEngine;
+    d_decisionEngine = NULL;
 
     delete d_stats;
+    d_stats = NULL;
     delete d_statisticsRegistry;
+    d_statisticsRegistry = NULL;
 
     delete d_private;
+    d_private = NULL;
 
     delete d_userContext;
+    d_userContext = NULL;
 
   } catch(Exception& e) {
     Warning() << "CVC4 threw an exception during cleanup." << endl