(qe2) Segmentation fault (release) or Assertion violation at ../src/ast/ast.h Line: 721

[muchang]

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

[537] % z3 small.smt2
sat
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 721
idx < m_num_args
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[538] % z3release small.smt2
sat
Segmentation fault
[539] % z3s
z3san    z3str3    z3str3model  
[539] % z3san small.smt2
sat
ASAN:DEADLYSIGNAL
=================================================================
==116314==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x558a0abee7fb bp 0x7ffd4556c200 sp 0x7ffd4556c200 T0)
==116314==The signal is caused by a READ memory access.
==116314==Hint: address points to the zero page.
  #0 0x558a0abee7fa in ast::get_kind() const ../src/ast/ast.h:504
  #1 0x558a0abee7fa in get_sort(expr const*) ../src/ast/ast.cpp:423
  #2 0x558a0abee7fa in ast_manager::get_sort(expr const*) const ../src/ast/ast.h:1738
  #3 0x558a0abee7fa in ast_manager::is_bool(expr const*) const ../src/ast/ast.cpp:1773
  #4 0x558a07eb44ba in qe::pred_abs::abstract_atoms(expr*, qe::max_level&, ref_vector<expr, ast_manager>&) ../src/qe/qsat.cpp:273
  #5 0x558a07eccdc2 in qe::pred_abs::abstract_atoms(expr*, ref_vector<expr, ast_manager>&) ../src/qe/qsat.cpp:221
  #6 0x558a07eccdc2 in qe::qsat::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/qe/qsat.cpp:1290
  #7 0x558a09b043ea in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #8 0x558a09b066ed 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
  #9 0x558a098b67b0 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223
  #10 0x558a09845eb8 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
  #11 0x558a0984cb2c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
  #12 0x558a0984cb2c in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #13 0x558a098041c5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #14 0x558a06e94eb6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #15 0x558a06e6d7ae in main ../src/shell/main.cpp:352
  #16 0x7f73a4e17b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #17 0x558a06e81529 in _start (/home/suz/software/z3san/build-04232020225820-7597396/z3+0x1f7529)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:504 in ast::get_kind() const
==116314==ABORTING
[540] % 
[540] % cat small.smt2
(assert (ite distinct true true))
(check-sat)
(check-sat-using qe2)

OS: Ubuntu 18.04
Commit: 7597396