From 2507dbb96587b8a1a23fb36d8e201e8ac77350de Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sat, 6 Jun 2020 09:14:40 -0700 Subject: [PATCH] Fix destruction order in NodeManager (#4578) Fixes #4576. ASan was reporting memory leaks because the skolem manager was being destroyed after the attributes and zombies were already cleaned up in the destructor of NodeManager. This commit changes the destruction order to ensure that the skolem manager is destroyed before the rest of the cleanup. Note: this issue did not only make the benchmark in #4576 fail but several tests in our regressions. --- src/expr/node_manager.cpp | 4 +++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/quantifiers/issue4576.smt2 | 5 +++++ 3 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/quantifiers/issue4576.smt2 diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 6f8934645..b32c93313 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -171,6 +171,9 @@ NodeManager::~NodeManager() { NodeManagerScope nms(this); + // Destroy skolem manager before cleaning up attributes and zombies + d_skManager = nullptr; + { ScopedBool dontGC(d_inReclaimZombies); // hopefully by this point all SmtEngines have been deleted @@ -233,7 +236,6 @@ NodeManager::~NodeManager() { // defensive coding, in case destruction-order issues pop up (they often do) delete d_resourceManager; d_resourceManager = NULL; - d_skManager = nullptr; delete d_statisticsRegistry; d_statisticsRegistry = NULL; delete d_registrations; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e0ce456bc..29224803a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -742,6 +742,7 @@ set(regress_0_tests regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2 regress0/quantifiers/issue4437-unc-quant.smt2 regress0/quantifiers/issue4476-ext-rew.smt2 + regress0/quantifiers/issue4576.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macros-int-real.smt2 regress0/quantifiers/macros-real-arg.smt2 diff --git a/test/regress/regress0/quantifiers/issue4576.smt2 b/test/regress/regress0/quantifiers/issue4576.smt2 new file mode 100644 index 000000000..3cb99b84a --- /dev/null +++ b/test/regress/regress0/quantifiers/issue4576.smt2 @@ -0,0 +1,5 @@ +; EXPECT: unsat +(set-logic NRA) +(declare-const r0 Real) +(assert (exists ((q36 Real) (q37 Bool) (q38 Bool) (q39 Bool) (q40 Real) (q41 Bool)) (= 0.0 0.0 (/ 437686.0 r0) 0.0 0.96101))) +(check-sat) -- 2.30.2