Segmentation fault (release) or Assertion violation at ../src/util/vector.h Line: 375 (debug)

Hi, For this case, Z3 throws out a segmentation fault:
[551] % z3debug rewriter.flat=false small.smt2
ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 375
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[552] % z3release rewriter.flat=false small.smt2
Segmentation fault
[553] % z3san rewriter.flat=false small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==14196==ERROR: AddressSanitizer: SEGV on unknown address 0x60e400003848 (pc 0x55949133f6f4 bp 0x7ffcc56f7dd0 sp 0x7ffcc56f7780 T0)
==14196==The signal is caused by a READ memory access.
  #0 0x55949133f6f3 in smt::theory_lra::imp::nl_value(int, _scoped_numeral<algebraic_numbers::manager>&) ../src/smt/theory_lra.cpp:3371
  #1 0x55949131d0dc in smt::theory_lra::imp::mk_value(smt::enode*, smt::model_generator&) ../src/smt/theory_lra.cpp:3399
  #2 0x55949131d0dc in smt::theory_lra::mk_value(smt::enode*, smt::model_generator&) ../src/smt/theory_lra.cpp:3955
  #3 0x559491399f41 in smt::model_generator::mk_value_procs(obj_map<smt::enode, smt::model_value_proc*>&, ptr_vector<smt::enode>&, ptr_vector<smt::model_value_proc>&) ../src/smt/smt_model_generator.cpp:113
  #4 0x55949139bb59 in smt::model_generator::mk_values() ../src/smt/smt_model_generator.cpp:297
  #5 0x5594913a089a in smt::model_generator::mk_model() ../src/smt/smt_model_generator.cpp:500
  #6 0x5594913c9b97 in smt::context::mk_proto_model() ../src/smt/smt_context.cpp:4456
  #7 0x5594913e187f in smt::context::get_model(ref<model>&) ../src/smt/smt_context.cpp:4487
  #8 0x55949102b9b6 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:224
  #9 0x559492a6f687 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #10 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #11 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #12 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #13 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #14 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #15 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #16 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #17 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #18 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #19 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #20 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #21 0x559492a620f1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #22 0x559492a6f687 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #23 0x559492a2b0da in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
  #24 0x559492a2d3dd 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 0x559492898ed8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #26 0x5594928b7df7 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #27 0x5594928cb624 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #28 0x5594928a69f1 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #29 0x5594928214f0 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1549
  #30 0x55949273cc63 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
  #31 0x55949273cc63 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
  #32 0x55949273cc63 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #33 0x5594926f4255 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #34 0x55948fddadc6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #35 0x55948fd937be in main ../src/shell/main.cpp:352
  #36 0x7f2342d24b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #37 0x55948fda7969 in _start (/local/suz-local/software/z3san/build-05112020173930-a14c2a3/z3+0x211969)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/smt/theory_lra.cpp:3371 in smt::theory_lra::imp::nl_value(int, _scoped_numeral<algebraic_numbers::manager>&)
==14196==ABORTING
[554] % 
[554] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun g () Real)
(declare-fun e () Real)
(define-fun h () Bool (and (> c 0) (= (+ e (div d b) g) (+ (* a a) c a))))
(define-fun f () Bool (= (+ g e) 0))
(assert h)
(assert (not f))
(check-sat)
[555] %
OS: Ubuntu 18.04 Commit: a14c2a3
Z3Prover / z3

Segmentation fault (release) or Assertion violation at ../src/util/vector.h Line: 375 (debug) #4295
