nlsat memory leak for QF_BV instance

[rainoftime]

Hi, for the following formula

(set-logic QF_BV)
(set-option :smt.clause_proof true)
(set-option :nlsat.log_lemmas true)
(set-option :nlsat.check_lemmas true)
(set-option :nlsat.randomize false)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const bv_3-0 (_ BitVec 3))
(push 1)
(declare-const v8 Bool)
(declare-const v9 Bool)
(assert (or v6 (= v3 v3) v3))
(assert (or (= v3 v3) v2 v4))
(assert (or v3 v3 v2))
(assert (or v1 (and (= v3 v3) v2 (= v3 v3)) v2))
(assert (or v4 (distinct #x2ed #x2ed #x2ed) (not (bvult #x2ed #x2ed))))
(assert (or v2 (not (bvult #x2ed #x2ed)) v7))
(assert (or (and (= v3 v3) v2 (= v3 v3)) v3 v5))
(assert (or (= v3 v3) (not (bvult #x2ed #x2ed)) (= v3 v3)))
(assert (or (xor v5 (= v0 v0 v2 v0 v0 v3 v1 v0 v2 v3 v1) v1 (bvule #x2ed #x2ed) v2) v7 v1))
(assert (or v1 v5 v7))
(assert (or v4 (= v0 v0 v2 v0 v0 v3 v1 v0 v2 v3 v1) (distinct #x2ed #x2ed #x2ed)))
(assert (or (= v0 v0 v2 v0 v0 v3 v1 v0 v2 v3 v1) v3 (= v0 v0 v2 v0 v0 v3 v1 v0 v2 v3 v1)))
(check-sat-using (then simplify bit-blast (par-or qfnra qfuf nlsat)))

z3 commit 2ac8d346 throws a leak

==50068==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 44 byte(s) in 1 object(s) allocated from:
    #0 0x7fbabdc60b90 in __interceptor_malloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeb90)
    #1 0x2bcfc2b in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x2c61335 in small_object_allocator::allocate(unsigned long) ../src/util/small_object_allocator.cpp:103
    #3 0x249281d in nlsat::solver::imp::mk_clause_core(unsigned int, sat::literal const*, bool, dependency_manager<nlsat::solver::imp::dconfig>
::dependency*) ../src/nlsat/nlsat_solver.cpp:920
    #4 0x2492a53 in nlsat::solver::imp::mk_clause(unsigned int, sat::literal const*, bool, dependency_manager<nlsat::solver::imp::dconfig>::dep
endency*) ../src/nlsat/nlsat_solver.cpp:930
    #5 0x24a2e34 in nlsat::solver::imp::resolve(nlsat::clause const&) ../src/nlsat/nlsat_solver.cpp:2113
    #6 0x249adf2 in nlsat::solver::imp::search() ../src/nlsat/nlsat_solver.cpp:1523
    #7 0x249b315 in nlsat::solver::imp::search_check() ../src/nlsat/nlsat_solver.cpp:1545
    #8 0x249caf4 in nlsat::solver::imp::check() ../src/nlsat/nlsat_solver.cpp:1619
    #9 0x2484c93 in nlsat::solver::check() ../src/nlsat/nlsat_solver.cpp:3484
    #10 0x19f8bef in nlsat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/nlsat/tactic/nlsat_tactic.cpp:159
    #11 0x19f97f4 in nlsat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/nlsat/tactic/nlsat_tactic.cpp:241
    #12 0x1e39057 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:909
    #13 0x1e30265 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #14 0x1e30265 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #15 0x1e30265 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #16 0x1e30265 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #17 0x1e30265 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #18 0x1e30265 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #19 0x1e30265 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #20 0x1e30265 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #21 0x1e393f8 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:933
    #22 0x1e318d1 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:296
    #23 0x1e30265 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #24 0x1e30265 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #25 0x1e31f2b in par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda(unsigned int)#1}::operator()(unsigned int) co
nst ../src/tactic/tactical.cpp:419
    #26 0x1e32a66 in par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}::operator()() const ../src/tactic/tactic
al.cpp:466
    #27 0x1e3d668 in void std::__invoke_impl<void, par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}>(std::__in
voke_other, par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}&&) /usr/include/c++/7/bits/invoke.h:60
    #28 0x1e3b9e3 in std::__invoke_result<par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}>::type std::__invok
e<par_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&)::{lambda()#2}>(std::__invoke_result&&, (par_tactical::operator()(ref<goal
> const&, sref_buffer<goal, 16u>&)::{lambda()#2}&&)...) /usr/include/c++/7/bits/invoke.h:95

[NikolajBjorner]

sorry, but this is squeezing blood out of stones: These guys are for debugging purposes:

(set-option :nlsat.log_lemmas true)
(set-option :nlsat.check_lemmas true)

Then on top of that you are running some threads in parallel. When one thread finishes, it will cause others to cancel. This is almost for sure the source of the leak as the debugging facilities may not be exception safe with respect to local memory usage. It isn't an objective to ensure that the debugging features have clean exception behavior. They are used to zero in on issues with the mainstream code.

I don't have bandwidth to annotate z3 with detailed information that you should not be using such flags. The general approach is that "if you choose to tweak with flags you better know what you are doing in the first place". It isn't ideal, but a function of what can be documented. Users are invited to add pull requests with documentation hints as well.

So just please don't file bugs with such combinations (trace + threads, log_lemmas, check_lemmas, ddfw, etc). It makes no sense to spend precious time on: you are four to six guys, probably stiff bored by home confinement, spewing out reports that affect random places in z3 by tweaking parameters and exploring variants of examples that bear a very faint scent of user realism. There are not four to six guys on the receiving end. These bugs come with very nice effort on minimization, but without any efforts devoted to identifying root causes. While many of these bug reports contribute to making z3 solid for unsuspecting and innocent users, which is great, it is also a constant source of noise, distraction and time sink. Recently, in more and more cases it is not clear at all whether it is time well spent to plug all and every weird hole. Basically, in many cases I am not sure a single real user of Z3 would benefit. There are many good things coming out: proof objects are getting scrutinized, and arith.solver=6 is exercised much more than simply running on SMTLIB benchmarks provide. Keeping it real is superb. So to be clear, thanks again for the many real bugs that you filed, but an effort to tone down the noise would be appreciated.

[zhendongsu]

Nikolaj, your direct, honest comments are appreciated as they were also partially directed at us :) We will do our best (meaning to the best of our understanding) to focus on filing interesting bugs. As always, your tireless effort is greatly appreciated! @NikolajBjorner @muchang @wintered