Assertion violation at src/ast/rewriter/seq_rewriter.cpp:460

[wintered]

[632] % z3 small.smt2 
ASSERTION VIOLATION
File: ../src/ast/rewriter/seq_rewriter.cpp
Line: 460
num_args == 2
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[633] % z3release small.smt2 
Segmentation fault
[634] % z3san small.smt2 
=================================================================
==2834==ERROR: AddressSanitizer: heap-buffer-overflow on address 0x60300000f180 at pc 0x5647f49bcebf bp 0x7ffefd598850 sp 0x7ffefd598840
READ of size 8 at 0x60300000f180 thread T0
  #0 0x5647f49bcebe in seq_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/seq_rewriter.cpp:461
  #1 0x5647f48409c3 in reduce_app_core ../src/ast/rewriter/th_rewriter.cpp:223
  #2 0x5647f48409c3 in reduce_app ../src/ast/rewriter/th_rewriter.cpp:620
  #3 0x5647f4849e6a in process_app<false> ../src/ast/rewriter/rewriter_def.h:298
  #4 0x5647f4849e6a in resume_core<false> ../src/ast/rewriter/rewriter_def.h:769
  #5 0x5647f4859eba in main_loop<false> ../src/ast/rewriter/rewriter_def.h:728
  #6 0x5647f4859eba in operator() ../src/ast/rewriter/rewriter_def.h:800
  #7 0x5647f4859eba in th_rewriter::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/th_rewriter.cpp:860
  #8 0x5647f31f4abb in asserted_formulas::assert_expr(expr*, app*) ../src/smt/asserted_formulas.cpp:158
  #9 0x5647f2ce0b4c in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:2901
  #10 0x5647f2ce0b4c in smt::context::assert_expr(expr*, app*) ../src/smt/smt_context.cpp:2913
  #11 0x5647f2ce0b4c in smt::context::assert_expr(expr*) ../src/smt/smt_context.cpp:2908
  #12 0x5647f441279c in solver::assert_expr(expr*) ../src/solver/solver.cpp:210
  #13 0x5647f441279c in solver::assert_expr(expr*) ../src/solver/solver.cpp:210
  #14 0x5647f43490c8 in cmd_context::assert_expr(expr*) ../src/cmd_context/cmd_context.cpp:1319
  #15 0x5647f42aaf58 in smt2::parser::parse_assert() ../src/parsers/smt2/smt2parser.cpp:2571
  #16 0x5647f42b16f7 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2926
  #17 0x5647f42b16f7 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #18 0x5647f4268b85 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #19 0x5647f18fa886 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #20 0x5647f18d30be in main ../src/shell/main.cpp:352
  #21 0x7f6619894b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #22 0x5647f18e6ef9 in _start (/home/suz/software/z3san/build-04272020171048-38e0968/z3+0x1f7ef9)
...
SUMMARY: AddressSanitizer: heap-buffer-overflow ../src/ast/rewriter/seq_rewriter.cpp:461 in seq_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&)
...
==2834==ABORTING
[635] % 
[635] % cat small.smt2 
(declare-fun a () String)
(assert (str.in.re a (re.inter (str.to.re "a"))))
(check-sat)
[636] %

OS: Ubuntu 18.04
Commit: b571e43