(proof, rewriter.eq2ineq, smt.arith.eager_eq_axioms, smt.arith.solver=2) Segmentation fault on QF_SLIA formula

Hi, For this case, Z3 throws out a segmentation fault:
[876] % z3 small.smt2
Segmentation fault
[877] % z3release small.smt2
unknown
[878] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==18695==ERROR: AddressSanitizer: SEGV on unknown address 0x00000000002c (pc 0x5654e01f66f7 bp 0x7ffc3e56b200 sp 0x7ffc3e56af40 T0)
==18695==The signal is caused by a READ memory access.
==18695==Hint: address points to the zero page.
  #0 0x5654e01f66f6 in smt::enode::merge_tf() const ../src/smt/smt_enode.h:130
  #1 0x5654e01f66f6 in smt::context::propagate_bool_var_enode(int) ../src/smt/smt_context.cpp:1394
  #2 0x5654e01f76d4 in smt::context::propagate_atoms() ../src/smt/smt_context.cpp:1310
  #3 0x5654e0203045 in smt::context::propagate() ../src/smt/smt_context.cpp:1675
  #4 0x5654e020f4c1 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3716
  #5 0x5654e020ff67 in smt::context::search() ../src/smt/smt_context.cpp:3600
  #6 0x5654e0211fc9 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3483
  #7 0x5654e0212ca1 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3419
  #8 0x5654e009425f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
  #9 0x5654e1b19c87 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #10 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #11 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #12 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #13 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #14 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #15 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #16 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #17 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #18 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #19 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #20 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #21 0x5654e1b0c5e1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #22 0x5654e1b19c87 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #23 0x5654e1a7b67a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #24 0x5654e1a7d97d 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:168
  #25 0x5654e197c2d8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #26 0x5654e1983697 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #27 0x5654e19410a4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #28 0x5654e1922191 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #29 0x5654e187d250 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1551
  #30 0x5654e17c3f33 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
  #31 0x5654e17c3f33 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
  #32 0x5654e17c3f33 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #33 0x5654e177b455 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #34 0x5654dee19f66 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #35 0x5654dedf299e in main ../src/shell/main.cpp:352
  #36 0x7fc5a555eb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #37 0x5654dee065d9 in _start (/home/suz/software/z3san/build-04182020194526-bcbe802/z3+0x1f75d9)
AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/smt/smt_enode.h:130 in smt::enode::merge_tf() const
==18695==ABORTING
[879] % 
[879] % cat small.smt2
(set-option :proof true)
(set-option :rewriter.eq2ineq true)
(set-option :smt.arith.eager_eq_axioms false)
(set-option :smt.arith.solver 2)
(declare-fun a () Int)
(declare-fun b () String)
(declare-fun c () String)
(assert (distinct a 0))
(assert (= a (str.len b)))
(assert (= 7 (str.len c)))
(check-sat)
[880] %
OS: Ubuntu 18.04 Commit: bcbe802
Z3Prover / z3

(proof, rewriter.eq2ineq, smt.arith.eager_eq_axioms, smt.arith.solver=2) Segmentation fault on QF_SLIA formula #4020
