Memory leak on QF_FPLRA formula (opt)

[rainoftime]

Hi, for the following formula,

(set-logic QF_FPLRA)
(set-option :opt.priority box)
(declare-const fpv2 Float32)
(declare-const fpv3 Float32)
(declare-const fpv5 Float32)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const r1 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const r9 Real)
(declare-const r10 Real)
(push 1)
(declare-const r11 Real)
(declare-const r12 Real)
(declare-const v3 Bool)
(declare-const fpv13 Float32)
(assert (not (>= r4 r11 241.63444 r12)))
(assert (xor v2 v1 v1 (>= 2993.0 r4 628948.0) v0))
(push 1)
(assert (or (fp.leq ((_ to_fp 8 24) RNA 0.136742) (fp.div RNA fpv13 ((_ to_fp 8 24) RNE 587212.0)) ((_ to_fp 8 24) RTN 368768.0) fpv5 ((_ to_fp 8 24) RTZ 4.308358)) (=> v1 (= r10 2003667863.0 r9)) (not v1) (fp.eq ((_ to_fp 8 24) RNA 0.136742) ((_ to_fp 8 24) RTN 368768.0)) (>= r4 r11 241.63444 r12) v3 v1 (not (>= r4 r11 241.63444 r12)) v0 v0))
(maximize (- r4 r12))
(check-sat)

z3 (commit 7f1b147) throws a leak

=================================================================                                                                                                                                  [39/1582]
==22546==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 24 byte(s) in 1 object(s) allocated from:
    #0 0x7ff28c345662 in malloc (/usr/lib/x86_64-linux-gnu/libasan.so.2+0x98662)
    #1 0x25e3b35 in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:268
    #2 0x25e3658 in memory::allocate(char const*, int, char const*, unsigned long) ../src/util/memory_manager.cpp:207
    #3 0x1122ea8 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:104
    #4 0x112570b in smt::model_generator::mk_values() ../src/smt/smt_model_generator.cpp:297
    #5 0x1128c19 in smt::model_generator::mk_model() ../src/smt/smt_model_generator.cpp:500
    #6 0xfcccda in smt::context::mk_proto_model() ../src/smt/smt_context.cpp:4443
    #7 0xfcd327 in smt::context::get_model(ref<model>&) ../src/smt/smt_context.cpp:4474
    #8 0xd3525c in smt::kernel::imp::get_model(ref<model>&) ../src/smt/smt_kernel.cpp:136
    #9 0xd34030 in smt::kernel::get_model(ref<model>&) ../src/smt/smt_kernel.cpp:319
    #10 0x5c7363 in opt::opt_solver::get_model_core(ref<model>&) ../src/opt/opt_solver.cpp:331
    #11 0x45e950 in check_sat_result::get_model(ref<model>&) ../src/solver/check_sat_result.h:58
    #12 0x5c69d2 in opt::opt_solver::set_model(unsigned int) ../src/opt/opt_solver.cpp:282
    #13 0x5c6d79 in opt::opt_solver::decrement_value(unsigned int, inf_eps_rational<inf_rational>&) ../src/opt/opt_solver.cpp:295
    #14 0x5c6351 in opt::opt_solver::maximize_objective(unsigned int, obj_ref<expr, ast_manager>&) ../src/opt/opt_solver.cpp:267
    #15 0x5e6797 in opt::optsmt::geometric_lex(unsigned int, bool) ../src/opt/optsmt.cpp:220
    #16 0x5eac6d in opt::optsmt::lex(unsigned int, bool) ../src/opt/optsmt.cpp:502
    #17 0x57cee8 in opt::context::execute_min_max(unsigned int, bool, bool, bool) ../src/opt/opt_context.cpp:409
    #18 0x57d6a5 in opt::context::execute(opt::context::objective const&, bool, bool) ../src/opt/opt_context.cpp:435
    #19 0x57c003 in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:332
    #20 0x19a075f in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1525
    #21 0x193113b in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596