heap-use-after-free at ast.h:505 (no option)

[rainoftime]

Hi, for the following formula,

(set-logic QF_LIA)
(declare-fun _substvar_329_ () Bool)
(declare-fun _substvar_331_ () Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v5 Bool)
(declare-const v7 Bool)
(declare-const v12 Bool)
(assert (xor true true v7 false (=> v5 (and v2 v3 (xor v2 v3 v5 v7 v1 true false true))) v3 true v2 false))
(assert (or (xor true true v7 false (=> v5 (and v2 v3 (xor v2 v3 v5 v7 v1 true false true))) v3 true v2 false) v1))
(assert (or (=> v5 _substvar_331_) _substvar_329_))
(assert (or false (and (=> v12 v3) (xor v2 v3 v5 v7 v1 true false true) v5 v3) false))
(assert (or (and v5 (and v2 v3 (xor v2 v3 v5 v7 v1 true false true)) v3) (and true true v2 v3 (xor v2 v3 v5 v7 v1 true false true) true)))
(assert (or (and true true v2 v3 (xor v2 v3 v5 v7 v1 true false true) true) (=> v5 false)))
(assert v1)
(check-sat)

z3 (commit 5b6255e) throws a uaf

=================================================================
==143035==ERROR: AddressSanitizer: heap-use-after-free on address 0x607000001d14 at pc 0x000000468057 bp 0x7fff399b31a0 sp 0x7fff399b3190
READ of size 4 at 0x607000001d14 thread T0
    #0 0x468056 in ast::hash() const ../src/ast/ast.h:505
    #1 0x5c15c7 in obj_map<expr, unsigned int>::key_data::hash() const ../src/util/obj_hashtable.h:78
    #2 0x5c05c7 in obj_map<expr, unsigned int>::obj_map_entry::get_hash() const ../src/util/obj_hashtable.h:87
    #3 0x5c0343 in core_hashtable<obj_map<expr, unsigned int>::obj_map_entry, obj_hash<obj_map<expr, unsigned int>::key_data>, default_eq<obj_map<expr, unsigned int>::key_data> >::find_core(obj_map<expr, 
unsigned int>::key_data const&) const ../src/util/hashtable.h:507
    #4 0x5be67c in obj_map<expr, unsigned int>::find_core(expr*) const ../src/util/obj_hashtable.h:158
    #5 0x5bc698 in obj_map<expr, unsigned int>::find(expr*, unsigned int&) const ../src/util/obj_hashtable.h:162
    #6 0x17eed92 in num_occurs::get_num_occs(expr*) const ../src/ast/num_occurs.h:48
    #7 0x17ee1b1 in ctx_simplify_tactic::simplifier::shared(expr*) const ../src/tactic/core/ctx_simplify_tactic.cpp:122
    #8 0x17ed61b in ctx_propagate_assertions::assert_expr(expr*, bool) ../src/tactic/core/ctx_simplify_tactic.cpp:54
    #9 0x17f11c4 in ctx_simplify_tactic::imp::assert_expr(expr*, bool) ../src/tactic/core/ctx_simplify_tactic.cpp:307
    #10 0x17f36da in ctx_simplify_tactic::imp::process_goal(goal&) ../src/tactic/core/ctx_simplify_tactic.cpp:548
    #11 0x17f43b8 in ctx_simplify_tactic::imp::operator()(goal&) ../src/tactic/core/ctx_simplify_tactic.cpp:593
    #12 0x17ee824 in ctx_simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/core/ctx_simplify_tactic.cpp:627
    #13 0x1a6f55d in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:918
    #14 0x1a6df07 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:769
    #15 0x1a68100 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
    #16 0x1a6824f in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #17 0x1a6824f in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #18 0x1a68100 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
    #19 0x1a68100 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
    #20 0x1a6df07 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:769
    #21 0x1a62852 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #22 0x1a62ced in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::_
_cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:168
    #23 0x19e8d42 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
    #24 0x19ededf in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #25 0x19f4ddb in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
    #26 0x19f1f49 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #27 0x19aa8a8 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1549
    #28 0x193af77 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #29 0x193eed3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #30 0x19405e5 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #31 0x191f60a in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #32 0x43c366 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #33 0x454496 in main ../src/shell/main.cpp:352
    #34 0x7f9a64ac782f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #35 0x414b98 in _start (/home/peisen/test/tofuzz/z3-debug/build/z3+0x414b98)