[505] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 375
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[506] %
[506] % z3release small.smt2
Segmentation fault
[507] %
[507] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==19475==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x55eb6d3207e3 bp 0x7ffc2582c800 sp 0x7ffc2582bc30 T0)
==19475==The signal is caused by a READ memory access.
==19475==Hint: address points to the zero page.
  #0 0x55eb6d3207e2 in ast::get_kind() const ../src/ast/ast.h:504
  #1 0x55eb6d3207e2 in is_app_of(expr const*, int, int) ../src/ast/ast.h:1373
  #2 0x55eb6d3207e2 in seq_util::str::is_unit(expr const*) const ../src/ast/seq_decl_plugin.h:323
  #3 0x55eb6d3207e2 in seq_rewriter::mk_seq_index(expr*, expr*, expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:1265
  #4 0x55eb6d346036 in seq_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:528
  #5 0x55eb6d1cb403 in reduce_app_core ../src/ast/rewriter/th_rewriter.cpp:221
  #6 0x55eb6d1cb403 in reduce_app ../src/ast/rewriter/th_rewriter.cpp:616
  #7 0x55eb6d1d4dca in process_app<false> ../src/ast/rewriter/rewriter_def.h:299
  #8 0x55eb6d1d4dca in resume_core<false> ../src/ast/rewriter/rewriter_def.h:770
  #9 0x55eb6d1e3bba in main_loop<false> ../src/ast/rewriter/rewriter_def.h:729
  #10 0x55eb6d1e3bba in operator() ../src/ast/rewriter/rewriter_def.h:801
  #11 0x55eb6d1e3bba in th_rewriter::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/th_rewriter.cpp:855
  #12 0x55eb6bb79bab in asserted_formulas::assert_expr(expr*, app*) ../src/smt/asserted_formulas.cpp:156
  #13 0x55eb6b66572c in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:2898
  #14 0x55eb6b66572c in smt::context::assert_expr(expr*, app*) ../src/smt/smt_context.cpp:2910
  #15 0x55eb6b66572c in smt::context::assert_expr(expr*) ../src/smt/smt_context.cpp:2905
  #16 0x55eb6cd9d91c in solver::assert_expr(expr*) ../src/solver/solver.cpp:210
  #17 0x55eb6cd9d91c in solver::assert_expr(expr*) ../src/solver/solver.cpp:210
  #18 0x55eb6ccd4298 in cmd_context::assert_expr(expr*) ../src/cmd_context/cmd_context.cpp:1321
  #19 0x55eb6cc36208 in smt2::parser::parse_assert() ../src/parsers/smt2/smt2parser.cpp:2571
  #20 0x55eb6cc3c9a7 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2926
  #21 0x55eb6cc3c9a7 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #22 0x55eb6cbf3e35 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #23 0x55eb6a280e66 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #24 0x55eb6a25975e in main ../src/shell/main.cpp:352
  #25 0x7f812c3b4b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #26 0x55eb6a26d4d9 in _start (/home/suz/software/z3san/build-04222020135510-f94abf6/z3+0x1f74d9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:504 in ast::get_kind() const
==19475==ABORTING
[508] %
[508] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (distinct (str.at (str.replace a b "") (str.indexof "B" (str.replace a b "") 2)))
[509] %