Assertion violation at src/util/vector.h:370

[wintered]

[532] % z3 small.smt2
unknown
unknown
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 370
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[533] % z3release small.smt2
unknown
unknown
Segmentation fault
[534] % z3san small.smt2
unknown
unknown
ASAN:DEADLYSIGNAL
=================================================================
==6832==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x55ef49ffccdb bp 0x7ffdbbf0aff0 sp 0x7ffdbbf0ae20 T0)
==6832==The signal is caused by a READ memory access.
==6832==Hint: address points to the zero page.
  #0 0x55ef49ffccda in mpz_manager<true>::is_zero(mpz const&) ../src/util/mpz.h:444
  #1 0x55ef49ffccda in mpq_manager<true>::is_zero(mpz const&) ../src/util/mpq.h:175
  #2 0x55ef49ffccda in mpq_manager<true>::is_zero(mpq const&) ../src/util/mpq.h:185
  #3 0x55ef49ffccda in rational::is_zero() const ../src/util/rational.h:267
  #4 0x55ef49ffccda in inf_rational::is_zero() const ../src/util/inf_rational.h:278
  #5 0x55ef49ffccda in smt::theory_dense_diff_logic<smt::mi_ext>::fix_zero() ../src/smt/theory_dense_diff_logic_def.h:802
  #6 0x55ef4a00c4d1 in smt::theory_dense_diff_logic<smt::mi_ext>::init_model(smt::model_generator&) ../src/smt/theory_dense_diff_logic_def.h:826
  #7 0x55ef4a3a57a6 in smt::model_generator::init_model() ../src/smt/smt_model_generator.cpp:67
  #8 0x55ef4a3b82b2 in smt::model_generator::mk_model() ../src/smt/smt_model_generator.cpp:497
  #9 0x55ef49c3bcff in smt::context::mk_proto_model() ../src/smt/smt_context.cpp:4443
  #10 0x55ef49c5358f in smt::context::get_model(ref<model>&) ../src/smt/smt_context.cpp:4474
  #11 0x55ef4b3a0ebc in check_sat_result::get_model(ref<model>&) ../src/solver/check_sat_result.h:58
  #12 0x55ef4b3a0ebc in combined_solver::get_model_core(ref<model>&) ../src/solver/combined_solver.cpp:298
  #13 0x55ef4b2ebd38 in check_sat_result::get_model(ref<model>&) ../src/solver/check_sat_result.h:58
  #14 0x55ef4b2ebd38 in cmd_context::is_model_available(ref<model>&) const ../src/cmd_context/cmd_context.cpp:2064
  #15 0x55ef4b3264e2 in get_model_cmd::execute(cmd_context&) ../src/cmd_context/basic_cmds.cpp:116
  #16 0x55ef4b22d878 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895
  #17 0x55ef4b2344ec in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001
  #18 0x55ef4b2344ec in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #19 0x55ef4b1ebb85 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179 
  #20 0x55ef4887d886 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #21 0x55ef488560be in main ../src/shell/main.cpp:352
  #22 0x7f6b19f3db96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #23 0x55ef48869ef9 in _start (/home/suz/software/z3san/build-04272020171048-38e0968/z3+0x1f7ef9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/util/mpz.h:444 in mpz_manager<true>::is_zero(mpz const&)
==6832==ABORTING
[535] %
[535] % cat small.smt2
(set-option :smt.arith.solver 3)
(declare-fun a () String)
(assert (= (str.len a) 0))
(check-sat (= a ""))
(check-sat)
(get-model)
[536] %

OS: Ubuntu 18.04
Commit: 38e0968