Memory leak on ALL formulas at smt_model_generator.cpp:113 (smt.arith.solver 1)

[rainoftime]

Hi, for the following formula

(set-option :smt.arith.solver 1)
(declare-const v0 Bool)
(declare-const v4 Bool)
(declare-const v13 Bool)
(declare-const i4 Int)
(declare-const r4 Real)
(declare-const r5 Real)
(assert (! (not (exists ((q6 Bool) (q7 (Array Int Bool)) (q8 Int) (q9 (_ BitVec 9)) (q10 (Array (Array Int Bool) Bool)) (q11 Bool)) (not (= q9 #b111111110)))) :named IP_2))
(declare-const r7 Real)
(declare-const v20 Bool)
(assert (! (or (> r4 215.4 r5 (- 49296.0))) :named IP_3))
(assert (! (or v13 v20 (> r4 215.4 r5 (- 49296.0)) v20 v13) :named IP_4))
(assert (! (or v20 (>= 2216.0 0.25722 (- r7 7876.0 0.6676))) :named IP_56))
(assert (! (or (> r4 215.4 r5 (- 49296.0)) v0) :named IP_78))
(assert (! (or (> (abs i4) 67)) :named IP_80))
(assert (! (or v13 v0 v4) :named IP_94))
(check-sat-assuming (IP_56 IP_94))
(check-sat-assuming (IP_78 IP_80))
(check-sat-assuming (IP_3 IP_4))

Z3 (commit f2449df) throws a memory leak

unknown
unknown
unknown

=================================================================
==61025==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 72 byte(s) in 3 object(s) allocated from:
    #0 0x7f19d11e5662 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98662)
    #1 0x2613c89 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x26137ac in memory::allocate(char const*, int, char const*, unsigned long) ../src/util/memory_manager.cpp:207
    #3 0xd615a0 in smt::theory_diff_logic<smt::rdl_ext>::mk_value(smt::enode*, smt::model_generator&) (/home/peisen/test/tofuzz/z3-debug/build/z3+0xd615a0)
    #4 0x1131139 in smt::model_generator::mk_value_procs(obj_map<smt::enode, smt::model_value_proc*>&, ptr_vector<smt::enode>&, ptr_vector<smt::model_value_proc>&) ../src/smt/smt_model_generator.cpp:113
    #5 0x1133765 in smt::model_generator::mk_values() ../src/smt/smt_model_generator.cpp:297
    #6 0x1136c73 in smt::model_generator::mk_model() ../src/smt/smt_model_generator.cpp:500
    #7 0xfd0aa4 in smt::context::mk_proto_model() ../src/smt/smt_context.cpp:4454
    #8 0xfc7af5 in smt::context::restart(lbool&, unsigned int) ../src/smt/smt_context.cpp:3648
    #9 0xfc760e in smt::context::search() ../src/smt/smt_context.cpp:3619
    #10 0xfc5923 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3497
    #11 0xd35c8c in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #12 0xd348e9 in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296
    #13 0x10dd080 in check_sat_core2 ../src/smt/smt_solver.cpp:190
    #14 0x19f0ff9 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #15 0x19f79d3 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:213
    #16 0x19f5063 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #17 0x19ad9c2 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1549
    #18 0x193e23b in smt2::parser::parse_check_sat_assuming() ../src/parsers/smt2/smt2parser.cpp:2609
    #19 0x1942234 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2982
    #20 0x19436ff in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #21 0x1922724 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #22 0x43c3c6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #23 0x4544f6 in main ../src/shell/main.cpp:352
    #24 0x7f19d028282f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)

SUMMARY: AddressSanitizer: 72 byte(s) leaked in 3 allocation(s).

[rainoftime]

Another instance

(set-option :model_validate true)
(set-option :smt.arith.solver 1)
(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 v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const i6 Int)
(declare-const i13 Int)
(declare-const r0 Real)
(declare-const r9 Real)
(declare-const arr (Array Int Int))
(assert v3)
(assert (or (= i6 i13) (distinct 69088.0658 r9 0.0 r0 0.25127106) (< 52 24) (distinct v1 (and v7 v4 v7 v5 v8 v0 v4 v2 v8 v11) (= arr arr arr arr) v10 v11 v5 v10 (distinct 69088.0658 r9 0.0 r0 0.25127106) v10 v9 (>= 52 i13)) v8))
(push 1)
(assert v11)
(check-sat)