[556] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 209
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[557] % 
[557] % z3release small.smt2
Segmentation fault
[558] % 
[558] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==9105==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000001 (pc 0x55897bfe6bc7 bp 0x7ffe2dfefab0 sp 0x7ffe2dfefab0 T0)
==9105==The signal is caused by a READ memory access.
==9105==Hint: address points to the zero page.
  #0 0x55897bfe6bc6 in ast_table::push_erase(ast*) ../src/ast/ast.cpp:625
  #1 0x55897bffb40a in ast_manager::delete_node(ast*) ../src/ast/ast.cpp:1930
  #2 0x5589782ad4c8 in ast_manager::dec_ref(ast*) ../src/ast/ast.h:1693
  #3 0x5589782ad4c8 in ref_manager_wrapper<expr, ast_manager>::dec_ref(expr*) ../src/util/ref_vector.h:199
  #4 0x5589782ad4c8 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::dec_ref(expr*) ../src/util/ref_vector.h:37
  #5 0x5589782ad4c8 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::dec_range_ref(expr* const*, expr* const*) ../src/util/ref_vector.h:41
  #6 0x5589782ad4c8 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::~ref_vector_core() ../src/util/ref_vector.h:54
  #7 0x5589792734ab in ref_vector<expr, ast_manager>::~ref_vector() ../src/util/ref_vector.h:210
  #8 0x5589792734ab in qe::quant_elim_plugin::~quant_elim_plugin() ../src/qe/qe.cpp:1384
  #9 0x55897925a9f0 in void dealloc<qe::quant_elim_plugin>(qe::quant_elim_plugin*) ../src/util/memory_manager.h:96
  #10 0x558979290532 in void dealloc<qe::quant_elim_plugin>(qe::quant_elim_plugin*) ../src/util/memory_manager.h:95
  #11 0x558979290532 in scoped_ptr<qe::quant_elim_plugin>::~scoped_ptr() ../src/util/util.h:236
  #12 0x558979290532 in qe::quant_elim_new::eliminate_block(unsigned int, app* const*, obj_ref<expr, ast_manager>&, ref_vector<app, ast_manager>&, bool, qe::guarded_defs*) ../src/qe/qe.cpp:2154
  #13 0x558979290db9 in qe::quant_elim_new::eliminate_exists(unsigned int, app* const*, obj_ref<expr, ast_manager>&, ref_vector<app, ast_manager>&, bool, qe::guarded_defs*) ../src/qe/qe.cpp:2108
  #14 0x558979262e57 in qe::quant_elim_new::eliminate_exists_bind(unsigned int, app* const*, obj_ref<expr, ast_manager>&) ../src/qe/qe.cpp:2201
  #15 0x558979258717 in qe::quant_elim_new::eliminate(bool, unsigned int, app* const*, obj_ref<expr, ast_manager>&) ../src/qe/qe.cpp:2072
  #16 0x558979258717 in qe::expr_quant_elim::elim(obj_ref<expr, ast_manager>&) ../src/qe/qe.cpp:2349
  #17 0x55897925854c in qe::expr_quant_elim::elim(obj_ref<expr, ast_manager>&) ../src/qe/qe.cpp:2346
  #18 0x5589792598b7 in qe::expr_quant_elim::operator()(expr*, expr*, obj_ref<expr, ast_manager>&) ../src/qe/qe.cpp:2240
  #19 0x55897931c5fe in qe_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/qe/qe_tactic.cpp:65
  #20 0x55897931c5fe in qe_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/qe/qe_tactic.cpp:116
  #21 0x55897af61248 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:918
  #22 0x55897aed1a4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #23 0x55897aed3d4d 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
  #24 0x55897ac83b30 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
  #25 0x55897ac13238 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
  #26 0x55897ac19eac in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
  #27 0x55897ac19eac in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #28 0x55897abd1545 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #29 0x558978290946 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #30 0x55897826941e in main ../src/shell/main.cpp:352
  #31 0x7fca518b3b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #32 0x55897827cfb9 in _start (/home/suz/software/z3san/build-04142020192323-164a73f/z3+0x1f6fb9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.cpp:625 in ast_table::push_erase(ast*)
==9105==ABORTING
[559] % 
[559] % cat small.smt2
(set-option :smt.phase_selection 5)
(declare-datatypes ((a 0)) ((b (c (d a)))))
(declare-sort e)
(declare-fun f (e) a)
(declare-fun i (a a) Bool)
(assert (forall ((g e) (h a)) (i h (f g))))
(assert (forall ((g e)) (exists ((h a)) (= (c h) (f g)))))
(check-sat-using qe)
[560] %