Memory leaks on string formula

[merlinsun]

Hi,
For this instance, z3 6835522 debug build leaks memory.

$ z3 small.smt2
sat

=================================================================
==1763508==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 320 byte(s) in 8 object(s) allocated from:
    #0 0x7fbac614fbc8 in malloc (/lib/x86_64-linux-gnu/libasan.so.5+0x10dbc8)
    #1 0x559b37cea80d in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:273
    #2 0x559b37cea196 in memory::allocate(char const*, int, char const*, unsigned long) ../src/util/memory_manager.cpp:212
    #3 0x559b37677a3a in dd::solver::add(dd::pdd const&, dependency_manager<scoped_dependency_manager<unsigned int>::config>::dependency*) ../src/math/grobner/pdd_solver.cpp:364
    #4 0x559b372d53ce in nla::grobner::add_eq(dd::pdd&, dependency_manager<scoped_dependency_manager<unsigned int>::config>::dependency*) ../src/math/lp/nla_grobner.cpp:453
    #5 0x559b372d5e37 in nla::grobner::add_row(vector<lp::row_cell<rational>, true, unsigned int> const&) ../src/math/lp/nla_grobner.cpp:472
    #6 0x559b372d037b in nla::grobner::configure() ../src/math/lp/nla_grobner.cpp:210
    #7 0x559b372cdb6f in nla::grobner::operator()() ../src/math/lp/nla_grobner.cpp:42
    #8 0x559b372a7bb7 in nla::core::check(vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_core.cpp:1510
    #9 0x559b3721122c in nla::solver::check(vector<nla::lemma, true, unsigned int>&) ../src/math/lp/nla_solver.cpp:32
    #10 0x559b359ca903 in smt::theory_lra::imp::check_nla_continue() (/home/z3/build/z3+0x16c5903)
    #11 0x559b359cadcb in smt::theory_lra::imp::check_nla() (/home/z3/build/z3+0x16c5dcb)
    #12 0x559b359be1bf in smt::theory_lra::imp::final_check_eh() ../src/smt/theory_lra.cpp:1582
    #13 0x559b359991be in smt::theory_lra::final_check_eh() ../src/smt/theory_lra.cpp:3863
    #14 0x559b35af8b74 in smt::context::final_check() ../src/smt/smt_context.cpp:3986
    #15 0x559b35af7571 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3902
    #16 0x559b35af46d2 in smt::context::search() ../src/smt/smt_context.cpp:3733
    #17 0x559b35af2621 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3616
    #18 0x559b3596c9dc in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:128
    #19 0x559b35959964 in check_sat_core2 ../src/smt/smt_solver.cpp:200
    #20 0x559b36afda72 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #21 0x559b36b05e14 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:225
    #22 0x559b36b0c934 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318
    #23 0x559b36ab4477 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1692
    #24 0x559b36a4b754 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611
    #25 0x559b36a4fbe8 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953
    #26 0x559b36a51a3b in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3162
    #27 0x559b36a2720b in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3211
    #28 0x559b34a1f4c2 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #29 0x559b34a347b2 in main ../src/shell/main.cpp:371

SUMMARY: AddressSanitizer: 320 byte(s) leaked in 8 allocation(s).
$ cat small.smt2
(declare-const x Int)
(declare-const x4 Bool)
(declare-const x384773__fresh Int)
(declare-const x1 Int)
(declare-const x1957__fresh Int)
(declare-const x44 Bool)
(declare-fun var1697 () String)
(declare-fun var () Int)
(declare-fun var1693 () String)
(declare-fun var1699 () String)
(declare-fun var1700 () String)
(declare-fun var444 () String)
(assert x44)
(assert (not (xor (>= x 0) (>= x1 0) (>= x 0) x4 (str.contains (str.++ (str.++ "1cguWC6Kd" (str.replace_re var1697 re.all var444)) "K4") (str.replace_re (str.substr (str.substr (str.++ var444) 0 (* (str.len var1693) 45 x1957__fresh)) var x384773__fresh) re.none (str.++ var1700 (str.substr var1699 0 x384773__fresh)))))))
(push)
(check-sat)