[503] % z3debug small.smt2
unknown
[504] % z3debug smt.string_solver=z3str3 small.smt2
Segmentation fault
[505] % z3release smt.string_solver=z3str3 small.smt2
Segmentation fault
[506] % z3san smt.string_solver=z3str3 small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==2450==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x55ff78c7123f bp 0x7ffdac4f0640 sp 0x7ffdac4f01f0 T0)
==2450==The signal is caused by a READ memory access.
==2450==Hint: address points to the zero page.
  #0 0x55ff78c7123e in automaton<sym_expr, sym_expr_manager>::compress() ../src/math/automata/automaton.h:349
  #1 0x55ff78ea6964 in smt::theory_str::solve_regex_automata() ../src/smt/theory_str_regex.cpp:280
  #2 0x55ff78a2f33a in smt::theory_str::final_check_eh() ../src/smt/theory_str.cpp:8577
  #3 0x55ff784f0464 in smt::context::final_check() ../src/smt/smt_context.cpp:3874
  #4 0x55ff784ffb86 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3790
  #5 0x55ff78500487 in smt::context::search() ../src/smt/smt_context.cpp:3614
  #6 0x55ff78502511 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3497
  #7 0x55ff785031e1 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3433
  #8 0x55ff78124bff in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
  #9 0x55ff79b96fb7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #10 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #11 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #12 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #13 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #14 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #15 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #16 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #17 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #18 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #19 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #20 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #21 0x55ff79b89a21 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #22 0x55ff79b96fb7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #23 0x55ff79b52a0a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
  #24 0x55ff79b54d0d 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:170
  #25 0x55ff799c0588 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #26 0x55ff799df727 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #27 0x55ff799f2f54 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #28 0x55ff799ce321 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #29 0x55ff79948d30 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1549
  #30 0x55ff798644b3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2595
  #31 0x55ff798644b3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2937
  #32 0x55ff798644b3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3129
  #33 0x55ff7981ba95 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3178
  #34 0x55ff76ed5606 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #35 0x55ff76e8de6e in main ../src/shell/main.cpp:352
  #36 0x7fbe788fab96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #37 0x55ff76ea2179 in _start (/local/suz-local/software/z3san/build-05172020210850-1c760b0/z3+0x213179)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/math/automata/automaton.h:349 in automaton<sym_expr, sym_expr_manager>::compress()
==2450==ABORTING
[507] %
[507] % cat small.smt2
(assert (str.in.re "" (re.loop (str.to.re "") (- 1))))
(check-sat)
[508] %