(smt.phase_selection 52, qe) Segmentation fault (release) or Assertion violation (debug) at ../src/smt/smt_context.cpp Line: 1847

[muchang]

Hi,
For this case, Z3 release throws out a segmentation fault:

[569] % z3 small.smt2 
ASSERTION VIOLATION
File: ../src/smt/smt_context.cpp
Line: 1847
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[570] % 
[570] % z3release small.smt2 
Segmentation fault
[571] % 
[571] % z3san small.smt2 
=================================================================
==16242==ERROR: AddressSanitizer: unknown-crash on address 0x61800000f2a8 at pc 0x563e9e555dba bp 0x7ffe270afa30 sp 0x7ffe270afa20
READ of size 4 at 0x61800000f2a8 thread T0
  #0 0x563e9e555db9 in smt::context::decide() ../src/smt/smt_context.cpp:1794
  #1 0x563e9e57bc92 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3764
  #2 0x563e9e57c617 in smt::context::search() ../src/smt/smt_context.cpp:3594
  #3 0x563e9e57e669 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3477
  #4 0x563e9e183d7f in qe::quant_elim_plugin::check(unsigned int, app* const*, expr*, obj_ref<expr, ast_manager>&, bool, ref_vector<app, ast_manager>&, qe::guarded_defs*) ../src/qe/qe.cpp:1449
  #5 0x563e9e185c3f 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:2157
  #6 0x563e9e186db9 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
  #7 0x563e9e158e57 in qe::quant_elim_new::eliminate_exists_bind(unsigned int, app* const*, obj_ref<expr, ast_manager>&) ../src/qe/qe.cpp:2201
  #8 0x563e9e14ee80 in qe::quant_elim_new::eliminate_forall_bind(unsigned int, app* const*, obj_ref<expr, ast_manager>&) ../src/qe/qe.cpp:2209
  #9 0x563e9e14ee80 in qe::quant_elim_new::eliminate(bool, unsigned int, app* const*, obj_ref<expr, ast_manager>&) ../src/qe/qe.cpp:2069
  #10 0x563e9e14ee80 in qe::expr_quant_elim::elim(obj_ref<expr, ast_manager>&) ../src/qe/qe.cpp:2349
  #11 0x563e9e14f8b7 in qe::expr_quant_elim::operator()(expr*, expr*, obj_ref<expr, ast_manager>&) ../src/qe/qe.cpp:2240
  #12 0x563e9e2125fe in qe_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/qe/qe_tactic.cpp:65
  #13 0x563e9e2125fe in qe_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/qe/qe_tactic.cpp:116
  #14 0x563e9fe57248 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:918
  #15 0x563e9fdc7a4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #16 0x563e9fdc9d4d 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
  #17 0x563e9fb79b30 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
  #18 0x563e9fb09238 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
  #19 0x563e9fb0feac in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
  #20 0x563e9fb0feac in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #21 0x563e9fac7545 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #22 0x563e9d186946 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #23 0x563e9d15f41e in main ../src/shell/main.cpp:352
  #24 0x7f237a30bb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #25 0x563e9d172fb9 in _start (/home/suz/software/z3san/build-04142020192323-164a73f/z3+0x1f6fb9)
...
==16242==ABORTING
[572] % 
[572] % cat small.smt2 
(set-option :smt.phase_selection 52)
(declare-datatypes ((a 0)) ((b c)))
(declare-sort d)
(declare-fun g (d) a)
(assert (forall ((e d) (f a)) (= f (g e))))
(check-sat-using qe)
[573] %

OS: Ubuntu 18.04
Commit: 164a73f