Invalid write in ast::inc_ref()

[fumfel]

Invalid write in ast::inc_ref()

Tested on HEAD: e677030

Faulting input: (set-option:produce-proofs true"")(define-fun Int0oString((i Int))String(ite(< i 0)(str.++"-"(int.to.str(- i)))(int.to.str i)))(check-sat)(declare-fun int0()Int)(declare-fun strInt0()String)(assert(= strInt0(Int0oString int0)))(check-sat)

To reproduce: z3 -smt2 z3_iw

ASAN log:

==26581==ERROR: AddressSanitizer: SEGV on unknown address 0x00000003ec18 (pc 0x00000215e0e0 bp 0x7fff4053d390 sp 0x7fff4053d080 T0)
==26581==The signal is caused by a WRITE memory access.
    #0 0x215e0df in ast::inc_ref() XYZ/z3/build/../src/ast/ast.h:452:21
    #1 0x215e0df in ast_manager::inc_ref(ast*) XYZ/z3/build/../src/ast/ast.h:1581
    #2 0x215e0df in ref_manager_wrapper<app, ast_manager>::inc_ref(app*) XYZ/z3/build/../src/util/ref_vector.h:186
    #3 0x215e0df in ref_vector_core<app, ref_manager_wrapper<app, ast_manager> >::inc_ref(app*) XYZ/z3/build/../src/util/ref_vector.h:36
    #4 0x215e0df in ref_vector_core<app, ref_manager_wrapper<app, ast_manager> >::push_back(app*) XYZ/z3/build/../src/util/ref_vector.h:93
    #5 0x215e0df in smt::conflict_resolution::mk_proof(smt::enode*, smt::enode*) XYZ/z3/build/../src/smt/smt_conflict_resolution.cpp:1242
    #6 0x2147dcc in smt::conflict_resolution::mk_conflict_proof(smt::b_justification, smt::literal) XYZ/z3/build/../src/smt/smt_conflict_resolution.cpp:1281:21
    #7 0x214c694 in smt::conflict_resolution::finalize_resolve(smt::b_justification, smt::literal) XYZ/z3/build/../src/smt/smt_conflict_resolution.cpp:487:13
    #8 0x214f280 in smt::conflict_resolution::resolve(smt::b_justification, smt::literal) XYZ/z3/build/../src/smt/smt_conflict_resolution.cpp:598:9
    #9 0x1f5ff54 in smt::context::resolve_conflict() XYZ/z3/build/../src/smt/smt_context.cpp:3838:36
    #10 0x1f5b400 in smt::context::bounded_search() XYZ/z3/build/../src/smt/smt_context.cpp:3630:22
    #11 0x1f58ebd in smt::context::search() XYZ/z3/build/../src/smt/smt_context.cpp:3503:22
    #12 0x1f58306 in smt::context::check(unsigned int, expr* const*, bool, bool) XYZ/z3/build/../src/smt/smt_context.cpp:3405:25
    #13 0x436761a in solver_na2as::check_sat(unsigned int, expr* const*) XYZ/z3/build/../src/solver/solver_na2as.cpp:67:12
    #14 0x3e74d5c in cmd_context::check_sat(unsigned int, expr* const*) XYZ/z3/build/../src/cmd_context/cmd_context.cpp:1395:27
    #15 0x3d9c370 in smt2::parser::parse_check_sat() XYZ/z3/build/../src/parsers/smt2/smt2parser.cpp:2305:19
    #16 0x3d93f66 in smt2::parser::parse_cmd() XYZ/z3/build/../src/parsers/smt2/smt2parser.cpp:2645:17
    #17 0x3d8d856 in smt2::parser::operator()() XYZ/z3/build/../src/parsers/smt2/smt2parser.cpp:2807:29
    #18 0x3d8ac04 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) XYZ/z3/build/../src/parsers/smt2/smt2parser.cpp:2856:12
    #19 0x530bcb in read_smtlib2_commands(char const*) XYZ/z3/build/../src/shell/smtlib_frontend.cpp:129:18
    #20 0x5172ac in main XYZ/z3/build/../src/shell/main.cpp:358:28
    #21 0x7f9791a8882f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #22 0x43e368 in _start (/usr/bin/z3+0x43e368)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV XYZ/z3/build/../src/ast/ast.h:452:21 in ast::inc_ref()
==26581==ABORTING