-
Notifications
You must be signed in to change notification settings - Fork 1.6k
segfaults on simple invalid formula (recent regression) #5224
Copy link
Copy link
Closed
Description
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] %
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels