diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-06 09:14:40 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-06 11:14:40 -0500 |
| commit | 2507dbb96587b8a1a23fb36d8e201e8ac77350de (patch) | |
| tree | 2b140c841480267e5b06fdfd8ba3ceacd6dee14b /test | |
| parent | fd60da4a22f02f6f5b82cef3585240c1b33595e9 (diff) | |
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.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/issue4576.smt2 | 5 |
2 files changed, 6 insertions, 0 deletions
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) |