diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-11 13:00:36 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-11 13:00:36 -0400 |
| commit | 0189f4b0e62edefa2b93f9bd4991a0c15c6cc3d5 (patch) | |
| tree | bfc3068f94b08816167ee396e77c3369ddc8953d /src/expr/expr_manager_template.cpp | |
| parent | 5527b0c00639f24b11d5e1d4c69050d908b82400 (diff) | |
Some defensive programming at destruction time, and fix a latent dangling pointer bug.
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 4 |
1 files changed, 4 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 |