Seg fault at ast.h:504 for string formula (z3str3)

[rainoftime]

Hi, for the following formula

(set-option :smt.string_solver z3str3)
(declare-const Str0 String)
(declare-const Str1 String)
(declare-const Str6 String)
(declare-const Str10 String)
(assert (= true true true true true true (= Str1 (str.++ Str6 Str0) (str.++ Str0 "" Str10 "")) true true))
(push 1)

z3 (commit 080dbb1) throws a SEGV

==61269==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x000000472ba9 bp 0x7ffe8fc59bc0 sp 0x7ffe8fc59bb0 T0)
==61269==The signal is caused by a READ memory access.
==61269==Hint: address points to the zero page.
    #0 0x472ba8 in ast::get_kind() const ../src/ast/ast.h:504
    #1 0x27ca79a in get_sort(expr const*) ../src/ast/ast.cpp:423
    #2 0x4730c7 in ast_manager::get_sort(expr const*) const ../src/ast/ast.h:1738
    #3 0x27e194b in ast_manager::check_args(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2285
    #4 0x27e11b8 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2247
    #5 0x27e271a in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2349
    #6 0x27de8d7 in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:2026
    #7 0x27de922 in ast_manager::mk_app(int, int, unsigned int, expr* const*) ../src/ast/ast.cpp:2031
    #8 0x5e9efe in ast_manager::mk_or(unsigned int, expr* const*) ../src/ast/ast.h:2171
    #9 0x28aef55 in mk_or(ast_manager&, unsigned int, expr* const*) ../src/ast/ast_util.cpp:178
    #10 0x5e1dfd in mk_or(ref_vector<expr, ast_manager> const&) ../src/ast/ast_util.h:133
    #11 0x1378647 in smt::theory_str::process_concat_eq_type1(expr*, expr*) ../src/smt/theory_str.cpp:3636
    #12 0x136f7f0 in smt::theory_str::simplify_concat_equality(expr*, expr*) ../src/smt/theory_str.cpp:3046
    #13 0x13bc51e in smt::theory_str::check_eqc_concat_concat(std::set<expr*, std::less<expr*>, std::allocator<expr*> >&, std::set<expr*, std::
less<expr*>, std::allocator<expr*> >&) ../src/smt/theory_str.cpp:7470
    #14 0x13b9db8 in smt::theory_str::handle_equality(expr*, expr*) ../src/smt/theory_str.cpp:7346
    #15 0x13bf5cb in smt::theory_str::new_eq_eh(int, int) ../src/smt/theory_str.cpp:7671
    #16 0xe742b8 in smt::context::propagate_th_eqs() ../src/smt/smt_context.cpp:1609
    #17 0xe74f4a in smt::context::propagate() ../src/smt/smt_context.cpp:1676
    #18 0xe82a43 in smt::context::push() ../src/smt/smt_context.cpp:2839
    #19 0xe5e54a in smt::kernel::imp::push() ../src/smt/smt_kernel.cpp:95
    #20 0xe5cbd7 in smt::kernel::push() ../src/smt/smt_kernel.cpp:268
    #21 0x10cb727 in push_core ../src/smt/smt_solver.cpp:167
    #22 0x1dbd238 in solver_na2as::push() ../src/solver/solver_na2as.cpp:88
    #23 0x1db66f1 in combined_solver::push() ../src/solver/combined_solver.cpp:172
    #24 0x1d61611 in cmd_context::push() ../src/cmd_context/cmd_context.cpp:1393
    #25 0x1d61949 in cmd_context::push(unsigned int) ../src/cmd_context/cmd_context.cpp:1407
    #26 0x1ce07d5 in smt2::parser::parse_push() ../src/parsers/smt2/smt2parser.cpp:2524
    #27 0x1ce5968 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2942
    #28 0x1ce713b in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #29 0x1cc10c2 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:
3179
    #30 0x46f791 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89

[NikolajBjorner]

until older bugs are addressed and fixed, please don't spend our bandwidth on new z3str3 bugs.

[mtrberzi]

Seems like add_theory_assumptions() is not getting called when the search is started. I recall encountering another issue where I had a similar problem.

[NikolajBjorner]

add_theory_assumptions only gets called prior to search. a "push" operation causes unit propagation. The theory solver code should not assume that theory assumptions have been added when it is asked to propagate. There are several places in the code where it accesses the m_theoryStrOverlapAssumption_term. You would either have to ensure these places are safe. Alternatively, perhaps you can initialize the assumption to "true".

        loopDetected(false),
        m_theoryStrOverlapAssumption_term(m.mk_true(), m),
        contains_map(m),

[NikolajBjorner]

GIven that I pushed the above suggested modification to theory_str the crash is now gone and the issue can be considered resolved