Segfault on a nested re.loop formula

[muchang]

[548] % z3release small.smt2
Segmentation fault
[549] % z3debug small.smt2
unsat
[550] % z3san small.smt2
AddressSanitizer:DEADLYSIGNAL
=================================================================
==2397280==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000001 (pc 0x560f5965ae7f bp 0x7ffddb8ea6a0 sp 0x7ffddb8ea6a0 T0)
==2397280==The signal is caused by a READ memory access.
==2397280==Hint: address points to the zero page.
  #0 0x560f5965ae7f in ast_table::push_erase(ast*) ../src/ast/ast.cpp:572
  #1 0x560f5966b824 in ast_manager::delete_node(ast*) ../src/ast/ast.cpp:1804
  #2 0x560f587fcc57 in ast_manager::dec_ref(ast*) ../src/ast/ast.h:1654
  #3 0x560f587fcc57 in obj_ref<expr, ast_manager>::dec_ref() ../src/util/obj_ref.h:32
  #4 0x560f587fcc57 in obj_ref<expr, ast_manager>::~obj_ref() ../src/util/obj_ref.h:59
  #5 0x560f587fcc57 in seq_rewriter::mk_antimirov_deriv_concat(expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:3427
  #6 0x560f5881490e in seq_rewriter::mk_antimirov_deriv_rec(expr*, expr*, expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:3351
  #7 0x560f58816b48 in seq_rewriter::mk_antimirov_deriv(expr*, expr*, expr*) ../src/ast/rewriter/seq_rewriter.cpp:3194
  #8 0x560f5881f6ad in seq_rewriter::mk_str_in_regexp(expr*, expr*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:4557
  #9 0x560f5883f31c in seq_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:706
  #10 0x560f58a45d36 in reduce_app_core ../src/ast/rewriter/th_rewriter.cpp:226
  #11 0x560f58a45d36 in reduce_app ../src/ast/rewriter/th_rewriter.cpp:627
  #12 0x560f58a4e61c in process_app<false> ../src/ast/rewriter/rewriter_def.h:316
  #13 0x560f58a4e61c in resume_core<false> ../src/ast/rewriter/rewriter_def.h:783
  #14 0x560f58a4e61c in main_loop<false> ../src/ast/rewriter/rewriter_def.h:742
  #15 0x560f58a4e61c in operator() ../src/ast/rewriter/rewriter_def.h:822
  #16 0x560f58a5a741 in th_rewriter::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/th_rewriter.cpp:1011
  #17 0x560f5756a064 in asserted_formulas::assert_expr(expr*, app*) ../src/solver/assertions/asserted_formulas.cpp:170
  #18 0x560f567359c7 in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:3029
  #19 0x560f567359c7 in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:3021
  #20 0x560f567359c7 in smt::context::assert_expr(expr*, app*) ../src/smt/smt_context.cpp:3045
  #21 0x560f567359c7 in smt::context::assert_expr(expr*) ../src/smt/smt_context.cpp:3040
  #22 0x560f57d8dee5 in solver::assert_expr(expr*) ../src/solver/solver.cpp:205
  #23 0x560f57d8dee5 in solver::assert_expr(expr*) ../src/solver/solver.cpp:205
  #24 0x560f57c8aa58 in cmd_context::assert_expr(expr*) ../src/cmd_context/cmd_context.cpp:1550
  #25 0x560f57c4debc in smt2::parser::parse_assert() ../src/parsers/smt2/smt2parser.cpp:2608
  #26 0x560f57c590d7 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2961
  #27 0x560f57c590d7 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3191
  #28 0x560f57c04ffd in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3242
  #29 0x560f54ea7411 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:182
  #30 0x560f54e7c992 in main ../src/shell/main.cpp:384
  #31 0x7fb7cff01d8f (/lib/x86_64-linux-gnu/libc.so.6+0x29d8f)
  #32 0x7fb7cff01e3f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x29e3f)
  #33 0x560f54e97ac4 in _start (/local/home/suz/suz-local/software/z3san/build-06062024081119-49610f5/z3+0x7b0ac4)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.cpp:572 in ast_table::push_erase(ast*)
==2397280==ABORTING
[551] % cat small.smt2
(assert (str.in_re "0" ((_ re.loop 0 1) ((_ re.loop 0 1) (str.to_re "1")))))
(check-sat)

Changing one or both of the 1's in the two re.loop's to another constant makes the segfault disappear.

version: 35c1cac