(smt.core.minimize, qe2) heap-use-after-free at /src/ast/ast.h:501 on BV formula

[rainoftime]

Hi, for the following formula,
z3 89a6c7a

(set-option :smt.core.minimize true)
(declare-fun v4 () Bool)
(declare-fun v90 () Bool)
(assert (or v90 v4))
(assert (forall ((q418 (_ BitVec 4)) (q420 (_ BitVec 1)) (q422 (_ BitVec 1)) (q423 (_ BitVec 12)) (q425 (_ BitVec 1))) (or v4 (= q420 (_ bv0 1)) (bvsge q418 (_ bv1 4)) (bvult q423 ((_ sign_extend 4) (_ bv1 8))))))
(check-sat-using qe2)

./z3 delta.out.smt2
=================================================================
==9076==ERROR: AddressSanitizer: heap-use-after-free on address 0x6070000153b4 at pc 0x55f6e93152cd bp 0x7fff51abe900 sp 0x7fff51abe8f0
READ of size 4 at 0x6070000153b4 thread T0
    #0 0x55f6e93152cc in ast::hash() const ../src/ast/ast.h:501
    #1 0x55f6e94c4719 in obj_map<expr, expr*>::key_data::hash() const ../src/util/obj_hashtable.h:77
    #2 0x55f6e94c3a3b in obj_map<expr, expr*>::obj_map_entry::get_hash() const ../src/util/obj_hashtable.h:86
    #3 0x55f6e94c3c19 in core_hashtable<obj_map<expr, expr*>::obj_map_entry, obj_hash<obj_map<expr, expr*>::key_data>, default_eq<obj_map<expr, expr*>::key_data> >::find_core(obj_map<expr, expr*>::key_dat
a const&) const ../src/util/hashtable.h:517
    #4 0x55f6e94c253c in obj_map<expr, expr*>::find_core(expr*) const ../src/util/obj_hashtable.h:157
    #5 0x55f6e94c2bf4 in obj_map<expr, expr*>::find(expr*) ../src/util/obj_hashtable.h:175
    #6 0x55f6e9b15b50 in qe::pred_abs::mk_concrete(ref_vector<expr, ast_manager>&, obj_map<expr, expr*> const&) ../src/qe/qsat.cpp:442
    #7 0x55f6e9b15e80 in qe::pred_abs::pred2lit(ref_vector<expr, ast_manager>&) ../src/qe/qsat.cpp:447
    #8 0x55f6e9b1b5f0 in qe::qsat::get_core(ref_vector<expr, ast_manager>&, unsigned int) ../src/qe/qsat.cpp:840
    #9 0x55f6e9b1bd1c in qe::qsat::project_qe(ref_vector<expr, ast_manager>&) ../src/qe/qsat.cpp:909
    #10 0x55f6e9b19cd7 in qe::qsat::check_sat() ../src/qe/qsat.cpp:675
    #11 0x55f6e9b2151b in qe::qsat::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/qe/qsat.cpp:1310
    #12 0x55f6eaf2141f in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:788
    #13 0x55f6eaf63113 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #14 0x55f6eaf636a1 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>&, s
td::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src/tactic/tactic.cpp:170
    #15 0x55f6eae3f1e9 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:216
    #16 0x55f6eadf98fa in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2893
    #17 0x55f6eadfa1eb in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2999
    #18 0x55f6eadfb657 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3128
    #19 0x55f6eadd56e7 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3177
    #20 0x55f6e92a7321 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #21 0x55f6e92ae326 in main ../src/shell/main.cpp:372
    #22 0x7f53daafdb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)