heap-use-after-free on String formula at ast.h:504

[rainoftime]

Hi, for the following formula,

(set-option :proof true)
(set-option :parallel.enable true)
(set-option :smt.random_seed 1)
(set-option :smt.arith.solver 6)
(set-option :smt.phase_selection 0)
(set-option :smt.threads 4)
(declare-const v3 Bool)
(declare-const v11 Bool)
(declare-const v13 Bool)
(declare-const v15 Bool)
(declare-const Str0 String)
(assert (! (and v11 v11 v11 v3) :named IP_1))
(assert (! (xor v13 true v15 true true true v13) :named IP_2))
(check-sat)
(assert (>= (str.len Str0) 88))
(push 1)
(check-sat)

z3 (commit 3e9479d) throws a uaf

unknown                                                                                                                                                                                            [143/670]
=================================================================
==94303==ERROR: AddressSanitizer: heap-use-after-free on address 0x60600008726c at pc 0x00000046804b bp 0x7fffb12298f0 sp 0x7fffb12298e0
READ of size 4 at 0x60600008726c thread T0
    #0 0x46804a in ast::get_kind() const ../src/ast/ast.h:504
    #1 0x22710f6 in get_sort(expr const*) ../src/ast/ast.cpp:423
    #2 0x46856d in ast_manager::get_sort(expr const*) const ../src/ast/ast.h:1738
    #3 0x21fa10c in has_real_arg ../src/ast/arith_decl_plugin.cpp:498
    #4 0x21fa929 in arith_decl_plugin::mk_func_decl(int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/arith_decl_plugin.cpp:552
    #5 0x228211a in ast_manager::mk_func_decl(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:2018
    #6 0x228216d in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:2024
    #7 0x2282320 in ast_manager::mk_app(int, int, expr*, expr*) ../src/ast/ast.cpp:2040
    #8 0x58eec2 in arith_util::mk_le(expr*, expr*) const ../src/ast/arith_decl_plugin.h:423
    #9 0x158a557 in smt::seq_axioms::add_length_limit(expr*, unsigned int) ../src/smt/seq_axioms.cpp:748
    #10 0x14ec10e in smt::theory_seq::add_length_limit(expr*, unsigned int, bool) ../src/smt/theory_seq.cpp:3652
    #11 0x1502d3b in smt::theory_seq::relevant_eh(app*) ../src/smt/theory_seq.cpp:5432
    #12 0xfad4b7 in smt::context::relevant_eh(expr*) ../src/smt/smt_context.cpp:1559                                                                                                               [127/670]
    #13 0x10b9448 in smt::relevancy_propagator_imp::set_relevant(expr*) ../src/smt/smt_relevancy.cpp:308
    #14 0x10b94fd in smt::relevancy_propagator_imp::mark_as_relevant(expr*) ../src/smt/smt_relevancy.cpp:336
    #15 0xd143d4 in smt::context::mark_as_relevant(expr*) ../src/smt/smt_context.h:1232
    #16 0xde9e93 in smt::context::mark_as_relevant(smt::enode*) ../src/smt/smt_context.h:1234
    #17 0x14f4332 in smt::theory_seq::mk_var(smt::enode*) ../src/smt/theory_seq.cpp:4400
    #18 0x14ebc34 in smt::theory_seq::internalize_term(app*) ../src/smt/theory_seq.cpp:3631
    #19 0x1010bdd in smt::context::internalize_theory_term(app*) ../src/smt/smt_internalizer.cpp:838
    #20 0x100fdb3 in smt::context::internalize_term(app*) ../src/smt/smt_internalizer.cpp:777
    #21 0x100bb57 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:358
    #22 0x100b5a0 in smt::context::internalize(expr*, bool) ../src/smt/smt_internalizer.cpp:339
    #23 0x11c192d in smt::theory_lra::imp::internalize_args(app*, bool) ../src/smt/theory_lra.cpp:684
    #24 0x11c1469 in smt::theory_lra::imp::linearize(smt::theory_lra::imp::scoped_internalize_state&) ../src/smt/theory_lra.cpp:654
    #25 0x11c0160 in smt::theory_lra::imp::linearize_term(expr*, smt::theory_lra::imp::scoped_internalize_state&) ../src/smt/theory_lra.cpp:529
    #26 0x11c3903 in smt::theory_lra::imp::internalize_def(app*) (/home/peisen/test/tofuzz/z3-debug/build/z3+0x11c3903)
    #27 0x11c5cb4 in smt::theory_lra::imp::internalize_atom(app*, bool) ../src/smt/theory_lra.cpp:1047
    #28 0x11b764a in smt::theory_lra::internalize_atom(app*, bool) ../src/smt/theory_lra.cpp:3932                                                                                                  [111/670]
    #29 0x100d333 in smt::context::internalize_theory_atom(app*, bool) ../src/smt/smt_internalizer.cpp:472
    #30 0x100c55f in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:411
    #31 0x100ba67 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350
    #32 0x100b5a0 in smt::context::internalize(expr*, bool) ../src/smt/smt_internalizer.cpp:339
    #33 0xfb35e3 in smt::context::reinit_clauses(unsigned int, unsigned int) ../src/smt/smt_context.cpp:2239
    #34 0xfb568f in smt::context::pop_scope_core(unsigned int) ../src/smt/smt_context.cpp:2413
    #35 0xfb5859 in smt::context::pop_scope(unsigned int) ../src/smt/smt_context.cpp:2421
    #36 0xfb59f0 in smt::context::pop_to_base_lvl() ../src/smt/smt_context.cpp:2429
    #37 0xf9e146 in smt::context::copy(smt::context&, smt::context&, bool) ../src/smt/smt_context.cpp:136
    #38 0x1133a3a in smt::parallel::operator()(ref_vector<expr, ast_manager> const&) ../src/smt/smt_parallel.cpp:74
    #39 0xfc142d in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3472
    #40 0xd3568c in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #41 0xd342ad in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296
    #42 0x10d6bf2 in check_sat_core2 ../src/smt/smt_solver.cpp:190
    #43 0x19e8f9f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67

[rainoftime]

Without asan, this leads to a segment fault .

[NikolajBjorner]

duplicate