Memory leak for QF_NIA formula (arith.solver 6)

[rainoftime]

Related: #3638

The issue only occurs in debug branch, but "it is still useful to address this."

---

Hi, for the following formula,

(set-logic QF_NIA)
(set-option :smt.arith.solver 6)
(declare-const v3 Bool)
(declare-const i1 Int)
(declare-const v16 Bool)
(assert (>= (mod 531 i1) (* 81 i1 i1 i1 i1)))
(assert (or v3 (> 0 (- (- (* 81 i1 i1 i1 i1) 81)))))
(assert (or v16 (= false false false (xor true false false true (<= i1 659) false false true true))))
(check-sat)

z3 (commit d5eef9d) throws a leak

sat

=================================================================
==6763==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 40 byte(s) in 1 object(s) allocated from:
    #0 0x7f1a84c48662 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98662)
    #1 0x25f7c2b in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x2627c39 in small_object_allocator::allocate(unsigned long) ../src/util/small_object_allocator.cpp:103
    #3 0x263fe37 in mpz_manager<false>::allocate(unsigned int) ../src/util/mpz.cpp:198
    #4 0x264ba4d in mpz_manager<false>::set_digits(mpz&, unsigned int, unsigned int const*) ../src/util/mpz.cpp:456
    #5 0x2640ef8 in mpz_manager<false>::set(mpz_cell&, mpz&, int, unsigned int) ../src/util/mpz.cpp:411
    #6 0x26423ea in mpz_manager<false>::big_mul(mpz const&, mpz const&, mpz&) ../src/util/mpz.cpp:781
    #7 0x26440d8 in mpz_manager<false>::mul(mpz const&, mpz const&, mpz&) ../src/util/mpz.cpp:506
    #8 0xda34ad in mpq_manager<false>::mul(mpq const&, mpq const&, mpq&) ../src/util/mpq.h:300
    #9 0x2626899 in mpq_manager<false>::power(mpq const&, unsigned int, mpq&) ../src/util/mpq.cpp:293
    #10 0x1eca023 in interval_manager<dep_intervals::im_config>::power(dep_intervals::im_config::interval const&, unsigned int, dep_intervals::im_config::interval&) ../src/math/interval/interval_def.h:1294
    #11 0x1ec7e8f in dep_intervals::im_config::interval dep_intervals::power<(dep_intervals::with_deps_t)1>(dep_intervals::im_config::interval const&, unsigned int) ../src/math/interval/dep_intervals.h:220
    #12 0x1ec3589 in void nla::intervals::to_power<(dep_intervals::with_deps_t)1>(_scoped_interval<dep_intervals>&, unsigned int) ../src/math/lp/nla_intervals.cpp:449
    #13 0x1ec0d50 in bool nla::intervals::interval_of_expr<(dep_intervals::with_deps_t)1, lp::explanation>(nla::nex const*, unsigned int, _scoped_interval<dep_intervals>&, std::function<void (lp::explanat
ion const&)> const&) ../src/math/lp/nla_intervals.cpp:480
    #14 0x1ec3c4d in bool nla::intervals::interval_of_mul<(dep_intervals::with_deps_t)1, lp::explanation>(nla::nex_mul const&, _scoped_interval<dep_intervals>&, std::function<void (lp::explanation const&)
> const&) ../src/math/lp/nla_intervals.cpp:424
    #15 0x1ec0cc4 in bool nla::intervals::interval_of_expr<(dep_intervals::with_deps_t)1, lp::explanation>(nla::nex const*, unsigned int, _scoped_interval<dep_intervals>&, std::function<void (lp::explanat
ion const&)> const&) ../src/math/lp/nla_intervals.cpp:470
    #16 0x1ec6d8e in bool nla::intervals::interval_of_sum_no_term<(dep_intervals::with_deps_t)1, lp::explanation>(nla::nex_sum const&, _scoped_interval<dep_intervals>&, std::function<void (lp::explanation const&)> const&) ../src/math/lp/nla_intervals.cpp:319
    #17 0x1ec2e3f in bool nla::intervals::interval_of_sum<(dep_intervals::with_deps_t)1, lp::explanation>(nla::nex_sum const&, _scoped_interval<dep_intervals>&, std::function<void (lp::explanation const&)> const&) ../src/math/lp/nla_intervals.cpp:370
    #18 0x1ec0c6b in bool nla::intervals::interval_of_expr<(dep_intervals::with_deps_t)1, lp::explanation>(nla::nex const*, unsigned int, _scoped_interval<dep_intervals>&, std::function<void (lp::explanat
ion const&)> const&) ../src/math/lp/nla_intervals.cpp:462
    #19 0x1eba861 in nla::intervals::check_nex(nla::nex const*, dependency_manager<scoped_dependency_manager<unsigned int>::config>::dependency*) ../src/math/lp/nla_intervals.cpp:90
    #20 0x1e578f0 in bool nla::horner::lemmas_on_row<vector<lp::row_cell<rational>, true, unsigned int> >(vector<lp::row_cell<rational>, true, unsigned int> const&)::{lambda(nla::nex const*)#1}::operator(
)(nla::nex const*) const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x1e578f0)
    #21 0x1e5c138 in std::_Function_handler<bool (nla::nex const*), bool nla::horner::lemmas_on_row<vector<lp::row_cell<rational>, true, unsigned int> >(vector<lp::row_cell<rational>, true, unsigned int> 
const&)::{lambda(nla::nex const*)#1}>::_M_invoke(std::_Any_data const&, nla::nex const*&&) /usr/include/c++/5/functional:1857
    #22 0x1e56f56 in std::function<bool (nla::nex const*)>::operator()(nla::nex const*) const (/home/peisen/test/tofuzz/z3-debug/build/z3+0x1e56f56)
    #23 0x1e51739 in nla::cross_nested::explore_expr_on_front_elem(nla::nex**, vector<nla::nex**, true, unsigned int>&) ../src/math/lp/cross_nested.h:256
    #24 0x1e4e837 in nla::cross_nested::run(nla::nex*) ../src/math/lp/cross_nested.h:70
    #25 0x1e4ac88 in nla::horner::lemmas_on_expr(nla::cross_nested&, nla::nex_sum*) ../src/math/lp/horner.cpp:68
    #26 0x1e57e1c in bool nla::horner::lemmas_on_row<vector<lp::row_cell<rational>, true, unsigned int> >(vector<lp::row_cell<rational>, true, unsigned int> const&) ../src/math/lp/horner.cpp:90
    #27 0x1e4b334 in nla::horner::horner_lemmas() ../src/math/lp/horner.cpp:121
    #28 0x1e22ac4 in nla::core::inner_check(bool) ../src/math/lp/nla_core.cpp:1300
    #29 0x1e2528a in nla::core::check(vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_core.cpp:1499

[NikolajBjorner]

fixed.
@levnach - I rewrote dep_intervals::power to pass output parameter as argument so that it could use scoped_dep_interval for memory management.