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

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 7ce51ecdd04562e5eb4dcd03ade3bf7dd3a7d21c..8bcfd58ba7003b5d2a907ba87eb0f54f3e2d1d5e 100644 (file)
--- 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 d0a477b9acd9b2ff8ab719887804ea9198e81d80..fb1284d0dfd262acb2224d8e883c5320296cd11e 100644 (file)
--- 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 2a12b07deb0d82400d13ee869151d46ed2a764a6..dcfc526eca3fbb9dd8799be6a1b9d1274103c29c 100644 (file)
--- 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