Segmentation fault QF_S formula

[wintered]

[664] % z3 small.smt2
Segmentation fault
[665] % z3release small.smt2
Segmentation fault
[666] % z3san small.smt2
=================================================================
==28375==ERROR: AddressSanitizer: unknown-crash on address 0x000000006250 at pc 0x55a420128b38 bp 0x7ffd200ca8c0 sp 0x7ffd200ca8b0
READ of size 8 at 0x000000006250 thread T0
  #0 0x55a420128b37 in get_sort(expr const*) ../src/ast/ast.cpp:425
  #1 0x55a420128b37 in ast_manager::get_sort(expr const*) const ../src/ast/ast.h:1738
  #2 0x55a420128b37 in ast_manager::coercion_needed(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2207
  #3 0x55a42014135c in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2235
  #4 0x55a42013fcb8 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2349
  #5 0x55a420148e90 in ast_manager::mk_app(int, int, expr*, expr*) ../src/ast/ast.cpp:2040
  #6 0x55a41e48156f in arith_util::mk_le(expr*, expr*) const ../src/ast/arith_decl_plugin.h:423
  #7 0x55a41e48156f in smt::seq_axioms::add_length_limit(expr*, unsigned int) ../src/smt/seq_axioms.cpp:748
  #8 0x55a41e2a432d in smt::theory_seq::add_length_limit(expr*, unsigned int, bool) ../src/smt/theory_seq.cpp:3652
  #9 0x55a41e2da03e in smt::theory_seq::relevant_eh(app*) ../src/smt/theory_seq.cpp:5432
  #10 0x55a41d771995 in smt::context::relevant_eh(expr*) ../src/smt/smt_context.cpp:1559
  #11 0x55a41d7ce389 in smt::relevancy_propagator_imp::set_relevant(expr*) ../src/smt/smt_relevancy.cpp:308
  #12 0x55a41d7ce389 in smt::relevancy_propagator_imp::mark_as_relevant(expr*) ../src/smt/smt_relevancy.cpp:336
  #13 0x55a41e2dab0c in smt::context::mark_as_relevant(expr*) ../src/smt/smt_context.h:1232
  #14 0x55a41e2dab0c in smt::context::mark_as_relevant(smt::enode*) ../src/smt/smt_context.h:1234
  #15 0x55a41e2dab0c in smt::theory_seq::mk_var(smt::enode*) ../src/smt/theory_seq.cpp:4400
  #16 0x55a41e2e39ba in smt::theory_seq::internalize_term(app*) ../src/smt/theory_seq.cpp:3631
  #17 0x55a41de4e05b in smt::context::internalize_theory_term(app*) ../src/smt/smt_internalizer.cpp:838
  #18 0x55a41de4e05b in smt::context::internalize_term(app*) ../src/smt/smt_internalizer.cpp:777
  #19 0x55a41de4e486 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:358
  #20 0x55a41de4e94e in smt::context::internalize_formula_core(app*, bool) ../src/smt/smt_internalizer.cpp:591
  #21 0x55a41de5387e in smt::context::internalize_eq(app*, bool) ../src/smt/smt_internalizer.cpp:425
  #22 0x55a41de5387e in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:408
  #23 0x55a41de4e4e9 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350
  #24 0x55a41de55dba in smt::context::internalize(expr*, bool) ../src/smt/smt_internalizer.cpp:339
  #25 0x55a41daa6fd4 in smt::theory::mk_eq(expr*, expr*, bool) ../src/smt/smt_theory.cpp:128
  #26 0x55a41e28499f in smt::theory_seq::branch_nq(smt::theory_seq::ne const&) ../src/smt/theory_seq.cpp:3177
  #27 0x55a41e29190a in smt::theory_seq::branch_nqs() ../src/smt/theory_seq.cpp:3157
  #28 0x55a41e2e1bce in smt::theory_seq::final_check_eh() ../src/smt/theory_seq.cpp:427
  #29 0x55a41d78f614 in smt::context::final_check() ../src/smt/smt_context.cpp:3857
  #30 0x55a41d79fb96 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3773
  #31 0x55a41d7a0497 in smt::context::search() ../src/smt/smt_context.cpp:3600
  #32 0x55a41d7a24f9 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3483
  #33 0x55a41d7a31d1 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3419
  #34 0x55a41d62478f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201
  #35 0x55a41f0aa257 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #36 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #37 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #38 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #39 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #40 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #41 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #42 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #43 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #44 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #45 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #46 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #47 0x55a41f09cbb1 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034
  #48 0x55a41f0aa257 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120
  #49 0x55a41f00bc4a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
  #50 0x55a41f00df4d 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
  #51 0x55a41ef0c8a8 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
  #52 0x55a41ef13c67 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
  #53 0x55a41eed1674 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
  #54 0x55a41eeb2761 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
  #55 0x55a41ee0d820 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1551
  #56 0x55a41ed54503 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
  #57 0x55a41ed54503 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
  #58 0x55a41ed54503 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
  #59 0x55a41ed0ba25 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
  #60 0x55a41c3aa466 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
  #61 0x55a41c382e3e in main ../src/shell/main.cpp:352
  #62 0x7f9ecd88ab96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
  #63 0x55a41c396ad9 in _start (/home/suz/software/z3san/build-04172020182140-3e9479d/z3+0x1f7ad9)
Address 0x000000006250 is a wild pointer.
SUMMARY: AddressSanitizer: unknown-crash ../src/ast/ast.cpp:425 in get_sort(expr const*)
...
==28375==ABORTING
[667] % 
[667] % cat small.smt2
(set-option :proof true)
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert (distinct a b))
(assert (distinct c (str.++ b "aaaaaaaaaaaaa")))
(check-sat)
[668] %

OS: Ubuntu 18.04
Commit: 3e9479d

[NikolajBjorner]

fixed