Skip to content

segfaults on simple invalid formula (recent regression) #5224

@zhendongsu

Description

@zhendongsu

Commit: 30e904b

[515] % z3-4.8.10 small.smt2
(error "line 1 column 9: invalid builtin application =")
[516] % z3debug small.smt2
Segmentation fault
[517] % z3release small.smt2
Segmentation fault
[518] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==26339==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x55f94a177c2b bp 0x7fff475295f0 sp 0x7fff475295f0 T0)
==26339==The signal is caused by a READ memory access.
==26339==Hint: address points to the zero page.
    #0 0x55f94a177c2a in ast::get_kind() const ../src/ast/ast.h:508
    #1 0x55f94a177c2a in expr::get_sort() const ../src/ast/ast.cpp:424
    #2 0x55f94a185053 in ast_manager::is_bool(expr const*) const ../src/ast/ast.cpp:1705
    #3 0x55f948b05d8b in smt2::parser::parse_assert() ../src/parsers/smt2/smt2parser.cpp:2572
    #4 0x55f948b108b7 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2935
    #5 0x55f948b108b7 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3139
    #6 0x55f948ac5f55 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3188
    #7 0x55f945e5596f in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #8 0x55f945e00357 in main ../src/shell/main.cpp:372
    #9 0x7f2953280b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #10 0x55f945e16109 in _start (/local/suz-local/software/z3san/build-04272021214656-30e904b/z3+0x206109)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/ast.h:508 in ast::get_kind() const
==26339==ABORTING
[519] % cat small.smt2
(assert =
[520] % 

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions