[528] % z3 small.smt2
Segmentation fault
[529] % z3release small.smt2
Segmentation fault
[530] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==29146==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x5605e1d5ed85 bp 0x7ffc1a197080 sp 0x7ffc1a197070 T0)
==29146==The signal is caused by a READ memory access.
==29146==Hint: address points to the zero page.
  #0 0x5605e1d5ed84 in ast::get_kind() const ../src/ast/ast.h:504
  #1 0x5605e1d5ed84 in get_sort(expr const*) ../src/ast/ast.cpp:423
  #2 0x5605e1d5ed84 in ast_manager::get_sort(expr const*) const ../src/ast/ast.h:1734
  #3 0x5605e1d5ed84 in basic_decl_plugin::check_proof_args(basic_op_kind, unsigned int, expr* const*) const ../src/ast/ast.cpp:771
  #4 0x5605e1daba5e in basic_decl_plugin::check_proof_args(basic_op_kind, unsigned int, expr* const*) const ../src/ast/ast.cpp:765
  #5 0x5605e1daba5e in basic_decl_plugin::mk_func_decl(int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:1196
  #6 0x5605e1d72ad2 in ast_manager::mk_func_decl(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:2009
  #7 0x5605e1daa6ca in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:2015
  #8 0x5605e1daa6ca in ast_manager::mk_th_lemma(int, expr*, unsigned int, app* const*, unsigned int, parameter const*) ../src/ast/ast.cpp:3366
  #9 0x5605e04c993b in purify_arith_proc::rw_cfg::push_cnstr_pr(app*) ../src/tactic/arith/purify_arith_tactic.cpp:263
  #10 0x5605e04e117d in purify_arith_proc::process_quantifier(quantifier*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/tactic/arith/purify_arith_tactic.cpp:748
  #11 0x5605e04e1a90 in purify_arith_proc::rw_cfg::get_subst(expr*, expr*&, app*&) ../src/tactic/arith/purify_arith_tactic.cpp:696
  #12 0x5605e04e1a90 in bool rewriter_tpl<purify_arith_proc::rw_cfg>::visit<true>(expr*, unsigned int) ../src/ast/rewriter/rewriter_def.h:140
  #13 0x5605e04e8074 in void rewriter_tpl<purify_arith_proc::rw_cfg>::main_loop<true>(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:715
  #14 0x5605e04ed601 in rewriter_tpl<purify_arith_proc::rw_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:798
  #15 0x5605e04ed601 in purify_arith_proc::operator()(ref<model_converter>&, bool) ../src/tactic/arith/purify_arith_tactic.cpp:761
  #16 0x5605e04f3abd in purify_arith_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/arith/purify_arith_tactic.cpp:908
  #17 0x5605e0d25f61 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111
  #18 0x5605e0d26f57 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #19 0x5605e0d26f57 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #20 0x5605e0c8894a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #21 0x5605e0c8ac4d 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
  #22 0x5605e0a3acc0 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
  #23 0x5605e09ca2e8 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
  #24 0x5605e09d0f5c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
  #25 0x5605e09d0f5c in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #26 0x5605e09885f5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #27 0x5605de01a1a6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #28 0x5605ddff2a3e in main ../src/shell/main.cpp:352
  #29 0x7fda2b8d7b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #30 0x5605de006819 in _start (/home/suz/software/z3san/build-04272020120633-8996e81/z3+0x1f7819)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:504 in ast::get_kind() const
==29146==ABORTING
[531] %
[531] % cat small.smt2
(set-option :proof true)
(assert (forall ((a Real)) (= a (/ 0 0))))
(check-sat-using purify-arith)
[532] %