heap-use-after-free at ast.h:504

[rainoftime]

Hi, for the following formula

(set-logic QF_BV)
(declare-const v14 Bool)
(assert v14)
(check-sat-using (then unit-subsume-simplify))                                 

z3 commit 2ac8d34 throws a uaf

==49800==ERROR: AddressSanitizer: heap-use-after-free on address 0x6070000033cc at pc 0x000000472b7f bp 0x7ffc21e2e020 sp 0x7ffc21e2e010
READ of size 4 at 0x6070000033cc thread T0
    #0 0x472b7e in ast::get_kind() const ../src/ast/ast.h:504
    #1 0x472e26 in is_app(ast const*) ../src/ast/ast.h:914
    #2 0x5bd17f in has_quantifiers(expr const*) ../src/ast/ast.h:1388
    #3 0xedd548 in asserted_formulas::assert_expr(expr*, app*) ../src/smt/asserted_formulas.cpp:166
    #4 0xedd8bd in asserted_formulas::assert_expr(expr*) ../src/smt/asserted_formulas.cpp:173
    #5 0xe76e84 in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:2957
    #6 0xe7722b in smt::context::assert_expr(expr*, app*) ../src/smt/smt_context.cpp:2969
    #7 0xe77141 in smt::context::assert_expr(expr*) ../src/smt/smt_context.cpp:2964
    #8 0xdb895e in unit_subsumption_tactic::prune_clause(unsigned int) ../src/smt/tactic/unit_subsumption_tactic.cpp:95
    #9 0xdb8873 in unit_subsumption_tactic::prune_clauses() ../src/smt/tactic/unit_subsumption_tactic.cpp:87
    #10 0xdb83bf in unit_subsumption_tactic::reduce_core(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/unit_subsumption_tactic.c
pp:69
    #11 0xdb817d in unit_subsumption_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/unit_subsumption_tactic.cp
p:46
    #12 0x1e37751 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:763
    #13 0x1e27667 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #14 0x1e27bf5 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manage
r::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src
/tactic/tactic.cpp:168
    #15 0x1d1de99 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
    #16 0x1cd6fa4 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
    #17 0x1cd7895 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
    #18 0x1cd8d1b in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #19 0x1cb2ca2 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:
3179
    #20 0x46f791 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #21 0x459a9c in main ../src/shell/main.cpp:352
    #22 0x7f9ea22cd82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)

[NikolajBjorner]

the stack doesn't look right: it uses nlsat, but I don't see this part of the code called at all for this input.

[rainoftime]

updated