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.

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 6f8934645be9b57f0ee22fa3312c9cec996a91e1..b32c9331309595ba5897f3024aba14da8d0e323e 100644 (file)
--- 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 e0ce456bc6cd19bec87ee84d3fece01bb37ae343..29224803ad25a01dd1ce918b431f1999089cd711 100644 (file)
--- 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 (file)
index 0000000..3cb99b8
--- /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)