heap-use-after-free at ../src/sat/sat_watched.h:87

[rainoftime]

Hi, for the following opt instance,
uaf_sat_watched87.txt

asan detects a heap-use-after-free in z3 master branch (Commit 5cbcd9a)

==5310==ERROR: AddressSanitizer: heap-use-after-free on address 0x6060000585a8 at pc 0x000001f42d45 bp 0x7ffce8c784c0 sp 0x7ffce8c784b0
READ of size 4 at 0x6060000585a8 thread T0
m    #0 0x1f42d44 in sat::watched::get_kind() const ../src/sat/sat_watched.h:87
    #1 0x1f42d69 in sat::watched::is_binary_clause() const ../src/sat/sat_watched.h:89
    #2 0x2100a73 in sat::probing::process_core(unsigned int) ../src/sat/sat_probing.cpp:165
    #3 0x2100cf1 in sat::probing::process(unsigned int) ../src/sat/sat_probing.cpp:185
    #4 0x21016e3 in sat::probing::operator()(bool) ../src/sat/sat_probing.cpp:257
    #5 0x1fcd5d5 in sat::solver::do_simplify() ../src/sat/sat_solver.cpp:1890
    #6 0x1fc4b9f in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1240
    #7 0xaa43e4 in inc_sat_solver::check_sat_core(unsigned int, expr* const*) ../src/sat/sat_solver/inc_sat_solver.cpp:199
    #8 0x197a883 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #9 0x57b24e in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:300
    #10 0x19319b5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1557
    #11 0x18c0611 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #12 0x18c45ad in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #13 0x18c5cbf in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #14 0x18a4ca4 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:
3179
    #15 0x45efb2 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #16 0x44f1aa in main ../src/shell/main.cpp:352
    #17 0x7f65add4082f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)