(proof) heap-use-after-free at ../src/ast/ast.h:500

Commit: 8abb644

(set-option :proof true)
(declare-fun v () (_ BitVec 5))
(declare-fun r () (Array (_ BitVec 5) Bool))
(assert-soft (select r v))
(assert-soft (select r (bvor v (bvand v (bvsdiv v (_ bv0 5))))))
(check-sat)

=================================================================                                                                                                                                           
==491460==ERROR: AddressSanitizer: heap-use-after-free on address 0x607000029f4c at pc 0x56069ee04875 bp 0x7ffe77a2fc10 sp 0x7ffe77a2fc00
READ of size 4 at 0x607000029f4c thread T0                                                                                                                                                                  
    #0 0x56069ee04874 in ast::get_kind() const ../src/ast/ast.h:500                                                                                                                                         
    #1 0x5606a1495197 in get_sort(expr const*) ../src/ast/ast.cpp:424                                                                                                                                       
    #2 0x56069edd59c3 in ast_manager::get_sort(expr const*) const ../src/ast/ast.h:1736     
    #3 0x5606a14ac60f in ast_manager::check_args(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2280
    #4 0x5606a14abe70 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2242
    #5 0x5606a14ad40f in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2344   
    #6 0x5606a14a945b in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:2021
    #7 0x5606a14a94a6 in ast_manager::mk_app(int, int, unsigned int, expr* const*) ../src/ast/ast.cpp:2026
    #8 0x56069edd5aac in ast_manager::mk_or(unsigned int, expr* const*) ../src/ast/ast.h:2194                                                                                                               
    #9 0x56069fdcea3e in smt::dyn_ack_cc_justification::mk_proof(smt::conflict_resolution&) ../src/smt/dyn_ack.cpp:97
    #10 0x56069fdfe319 in smt::conflict_resolution::mk_conflict_proof(smt::b_justification, smt::literal) ../src/smt/smt_conflict_resolution.cpp:1297
    #11 0x56069fdf1f53 in smt::conflict_resolution::finalize_resolve(smt::b_justification, smt::literal) ../src/smt/smt_conflict_resolution.cpp:479
    #12 0x56069fdf4097 in smt::conflict_resolution::resolve(smt::b_justification, smt::literal) ../src/smt/smt_conflict_resolution.cpp:599
    #13 0x56069f98e0d5 in smt::context::resolve_conflict() ../src/smt/smt_context.cpp:4026
    #14 0x56069f98b1ab in smt::context::bounded_search() ../src/smt/smt_context.cpp:3812
    #15 0x56069f9897e7 in smt::context::search() ../src/smt/smt_context.cpp:3691                                                                                                                            
    #16 0x56069f987d09 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3574           
    #17 0x56069f9ba522 in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116          
    #18 0x56069f9b7f2f in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:330              
    #19 0x56069efa07c5 in opt::opt_solver::check_sat_core2(unsigned int, expr* const*) ../src/opt/opt_solver.cpp:189
    #20 0x5606a09c317b in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #21 0x5606a09ae7ab in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:332
    #22 0x56069efa7a90 in solver::check_sat(ref_vector<expr, ast_manager> const&) ../src/solver/solver.h:151
    #23 0x56069efa88fb in opt::maxlex::maxlexN() ../src/opt/maxlex.cpp:159                 
    #24 0x56069efa8ecf in opt::maxlex::operator()() ../src/opt/maxlex.cpp:198                                                                                                                               
    #25 0x56069ef90848 in opt::maxsmt::operator()() ../src/opt/maxsmt.cpp:264          
    #26 0x56069ef4d37f in opt::context::execute_maxsat(symbol const&, bool, bool) ../src/opt/opt_context.cpp:428 
    #27 0x56069ef4d6d5 in opt::context::execute(opt::context::objective const&, bool, bool) ../src/opt/opt_context.cpp:442
    #28 0x56069ef4bd62 in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:335                            
    #29 0x5606a096a396 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1547
    #30 0x5606a090d99f in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2594
    #31 0x5606a0911d51 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2936                                                                                                                 
    #32 0x5606a09134f1 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3128                                                                                                                
    #33 0x5606a08ed825 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3177
    #34 0x56069edca783 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142                                                                                                           
    #35 0x56069ede05ba in main ../src/shell/main.cpp:372                                  
    #36 0x7f9cd6848151 in __libc_start_main (/usr/lib/libc.so.6+0x28151)

Z3Prover / z3

(proof) heap-use-after-free at ../src/ast/ast.h:500 #4952