[576] % z3release small.smt2
sat
[577] % z3debug smt.string_solver=z3str3 small.smt2
Segmentation fault
[578] % z3release smt.string_solver=z3str3 small.smt2
Segmentation fault
[579] % z3san smt.string_solver=z3str3 small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==16389==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x56103c6921fe bp 0x7ffd15509bd0 sp 0x7ffd15509b90 T0)
==16389==The signal is caused by a READ memory access.
==16389==Hint: address points to the zero page.
  #0 0x56103c6921fd in ast::get_kind() const ../src/ast/ast.h:505
  #1 0x56103c6921fd in is_app_of(expr const*, int, int) ../src/ast/ast.h:1374
  #2 0x56103c6921fd in bv_recognizers::is_numeral(expr const*, rational&, unsigned int&) const ../src/ast/bv_decl_plugin.cpp:784
  #3 0x56103c5e8d04 in seq_util::is_const_char(expr*, unsigned int&) const ../src/ast/seq_decl_plugin.cpp:1135
  #4 0x56103a77395d in smt::theory_str::aut_path_rewrite_constraint(expr*, expr*) ../src/smt/theory_str_regex.cpp:1379
  #5 0x56103a785eaa in smt::theory_str::generate_regex_path_constraints(expr*, automaton<sym_expr, sym_expr_manager>*, rational, obj_ref<expr, ast_manager>&) ../src/smt/theory_str_regex.cpp:1555
  #6 0x56103a794a1b in smt::theory_str::solve_regex_automata() ../src/smt/theory_str_regex.cpp:211
  #7 0x56103a31782a in smt::theory_str::final_check_eh() ../src/smt/theory_str.cpp:8577
  #8 0x561039dd8974 in smt::context::final_check() ../src/smt/smt_context.cpp:3874
  #9 0x561039de8096 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3790
  #10 0x561039de8997 in smt::context::search() ../src/smt/smt_context.cpp:3614
  #11 0x561039deaa21 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3497
  #12 0x561039deb6f1 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3433
  #13 0x561039a0b08f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
  #14 0x56103b47fc87 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122
  #15 0x56103b4726f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
  #16 0x56103b4726f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1053
...
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:505 in ast::get_kind() const
==16389==ABORTING
[580] % 
[580] % cat small.smt2
(set-logic QF_S)
(declare-fun a () String)
(assert (str.in_re a (re.range "a" "z")))
(assert (str.in_re (str.++ a "b") (re.comp (re.range "a" "z"))))
(check-sat)
[581] %