Segment fault at ast.h:504 for NIA instance (proof enabled)

[rainoftime]

Hi, for the following formula

(set-logic NIA)
(set-option :proof true)
(set-option :smt.mbqi false)
(declare-const v4 Bool)
(declare-const i7 Int)
(assert (not (forall ((q3 Int) (q4 Bool) (q5 Bool)) (=> (or v4 q4 q5 q5) (>= 114 (* i7 45))))))
(check-sat-using (then purify-arith ctx-solver-simplify add-bounds qflia))

z3 commit cf0952c throws a SEGV

ASAN:SIGSEGV
=================================================================
==141960==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x000000467a69 bp 0x7fff752ab600 sp 0x7fff752ab5f0 T0)
    #0 0x467a68 in ast::get_kind() const ../src/ast/ast.h:504
    #1 0x467d0c in is_app(ast const*) ../src/ast/ast.h:914
    #2 0x6e5acb in ast_manager::is_proof(expr const*) const ../src/ast/ast.h:2233
    #3 0x6e5bc3 in ast_manager::has_fact(app const*) const ../src/ast/ast.h:2277
    #4 0x21e7aa2 in ast_manager::mk_unit_resolution(unsigned int, app* const*) ../src/ast/ast.cpp:3102
    #5 0x19cbe82 in goal::elim_redundancies() ../src/tactic/goal.cpp:567
    #6 0x17bcb95 in simplify_tactic::imp::operator()(goal&) ../src/tactic/core/simplify_tactic.cpp:66
    #7 0x17bbe85 in simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/core/simplify_tactic.cpp:94
    #8 0x19df8e5 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:909
    #9 0x19d86b2 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
    #10 0x19d86b2 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
    #11 0x19d86b2 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
    #12 0x19de2f3 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:763
    #13 0x19d8801 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #14 0x19d8801 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #15 0x19d8801 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
    #16 0x19de2f3 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:763
    #17 0x19d3008 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #18 0x19d34a3 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
    #19 0x18e87cc in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
    #20 0x18af963 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
    #21 0x18b0174 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
    #22 0x18b154f in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #23 0x1890534 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #24 0x43c08e in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #25 0x453f22 in main ../src/shell/main.cpp:352
    #26 0x7faf550d882f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
    #27 0x414838 in _start (/home/peisen/test/tofuzz/z3-debug/build/z3+0x414838)

AddressSanitizer can not provide additional info.

[NikolajBjorner]

perhaps dup of #3612