Memory leak at old_interval.h:37 (opt, smt.phase_selection 0, smt.arith.solver 5) and (smt.arith.solver 2, ctx-solver-simplify)

[rainoftime]

Hi, for the following formula,
z3 (d6ad371) throws a leak

(set-option :smt.phase_selection 0)
(set-option :smt.arith.solver 5)
(declare-const v5 Bool)
(declare-const r1 Real)
(declare-const r6 Real)
(declare-const r8 Real)
(declare-const r10 Real)
(declare-const r12 Real)
(declare-const r13 Real)
(declare-const r14 Real)
(declare-const r16 Real)
(declare-const r18 Real)
(declare-const r19 Real)
(declare-const r20 Real)
(assert (or v5 (<= r10 (/ (/ (/ r6 r14) (/ 2297.0 15018372672.0)) 0.0)) (> r1 (/ r6 (/ 2297.0 15018372672.0)) r13 r18 r6)))
(minimize (+ r13 r14 r16))
(minimize (+ r13 r18 r20))
(maximize (- r8 r13 r19))
(minimize (+ r1 r6 r20))
(minimize (+ r1 r8 r14))
(minimize (+ r6 r12 r14))
(maximize (- r8 r16 r19))
(maximize (- r6 r8 r12))
(check-sat)

unknown

=================================================================
==47865==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 80 byte(s) in 2 object(s) allocated from:
    #0 0x7f77338bb662 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98662)
    #1 0x263c621 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x26730d4 in mpz_manager<true>::allocate(unsigned int) ../src/util/mpz.cpp:197
    #3 0x26757e9 in mpz_manager<true>::big_set(mpz&, mpz const&) ../src/util/mpz.cpp:1500
    #4 0x464d3b in mpz_manager<true>::set(mpz&, mpz const&) ../src/util/mpz.h:532
    #5 0x464a1c in mpq_manager<true>::set(mpz&, mpz const&) ../src/util/mpq.h:660
    #6 0x463670 in mpq_manager<true>::set(mpq&, mpq const&) ../src/util/mpq.h:663
    #7 0x461485 in rational::rational(rational const&) ../src/util/rational.h:43
    #8 0x815907 in ext_numeral::ext_numeral(ext_numeral const&) ../src/smt/old_interval.h:37
    #9 0x10c91c0 in old_interval::old_interval(old_interval const&) ../src/smt/old_interval.cpp:237
    #10 0xf62d5f in buffer<old_interval, true, 16u>::push_back(old_interval&&) ../src/util/buffer.h:160
    #11 0xf34f95 in smt::theory_arith<smt::inf_ext>::is_inconsistent2(grobner::equation const*, grobner&) ../src/smt/theory_arith_nl.h:1996
    #12 0xf37e75 in smt::theory_arith<smt::inf_ext>::get_gb_eqs_and_look_for_conflict(ptr_vector<grobner::equation>&, grobner&) ../src/smt/theory_arith_nl.h:2154
    #13 0xf373c0 in smt::theory_arith<smt::inf_ext>::compute_grobner(svector<int, unsigned int> const&) ../src/smt/theory_arith_nl.h:2257
    #14 0xf39982 in smt::theory_arith<smt::inf_ext>::process_non_linear() ../src/smt/theory_arith_nl.h:2357
    #15 0xef3aab in smt::theory_arith<smt::inf_ext>::final_check_core() ../src/smt/theory_arith_core.h:1461
    #16 0xef4246 in smt::theory_arith<smt::inf_ext>::final_check_eh() ../src/smt/theory_arith_core.h:1499
    #17 0xfe2c73 in smt::context::final_check() ../src/smt/smt_context.cpp:3874
    #18 0xfe1c7c in smt::context::bounded_search() ../src/smt/smt_context.cpp:3790
    #19 0xfdf38a in smt::context::search() ../src/smt/smt_context.cpp:3614
    #20 0xfdd917 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3497
    #21 0xd438aa in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #22 0xd42507 in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296
    #23 0x5c657d in opt::opt_solver::check_sat_core2(unsigned int, expr* const*) ../src/opt/opt_solver.cpp:189
    #24 0x1a03455 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #25 0x1a074bf in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #26 0x5e73d5 in opt::optsmt::geometric_lex(unsigned int, bool) ../src/opt/optsmt.cpp:214
    #27 0x5ebaa1 in opt::optsmt::lex(unsigned int, bool) ../src/opt/optsmt.cpp:502
    #28 0x57db6c in opt::context::execute_min_max(unsigned int, bool, bool, bool) ../src/opt/opt_context.cpp:412
    #29 0x57e383 in opt::context::execute(opt::context::objective const&, bool, bool) ../src/opt/opt_context.cpp:439

[rainoftime]

(set-option :smt.arith.solver 2)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v4 Bool)
(declare-const r0 Real)
(declare-const r4 Real)
(declare-const v9 Bool)
(assert (or (not (and v4 v2 v1 v4 v9))))
(assert (or (distinct (abs (- r4 (abs r0) (* r0 r0 r0) r0 0.79891)) (abs r0) (* r0 r0 r0))))
(check-sat-using (then simplify ctx-solver-simplify))

[NikolajBjorner]

@nunoplopes @danielschemmel
Not sure about the memory discipline in buffer.h
We have

    void expand() {
        unsigned new_capacity = m_capacity << 1;
        T * new_buffer        = reinterpret_cast<T*>(memory::allocate(sizeof(T) * new_capacity));
        for (unsigned i = 0; i < m_pos; ++i) {
            new (&new_buffer[i]) T(std::move(m_buffer[i]));
        }
        free_memory();
        m_buffer              = new_buffer;
        m_capacity            = new_capacity;
    }

so std::move is invoked on elements in the previous buffer and then it calls T(..), which
in this example is

interval::interval(interval const & other):
    m_manager(other.m_manager),
    m_lower(other.m_lower),
    m_upper(other.m_upper),
    m_lower_open(other.m_lower_open),
    m_upper_open(other.m_upper_open),
    m_lower_dep(other.m_lower_dep),
    m_upper_dep(other.m_upper_dep) {
}

So from what I can tell, resources allocated for m_lower and m_upper are copied over (and not moved) so the destructor should be invoked. ?