Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Z3 4.8.5 segfaults on aarch64 linux #3476

Open
gebner opened this issue Sep 14, 2024 · 0 comments
Open

Z3 4.8.5 segfaults on aarch64 linux #3476

gebner opened this issue Sep 14, 2024 · 0 comments

Comments

@gebner
Copy link
Contributor

gebner commented Sep 14, 2024

While Z3 4.8.5 builds on aarch64 linux, it segfaults already on the VCs from prims.fst:

  CHECK     prims.fst
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("Unexpexted output from Z3: no result section found:\nkilled")

This is the backtrace. (4.13.0 runs just fine for comparison.)

(gdb) bt
#0  0x0000000000c23b8c in smt::mam_impl::insert(smt::path_tree*, smt::path*, quantifier*, app*) ()
#1  0x0000000000c2458c in smt::mam_impl::update_filters(app*, smt::path*, quantifier*, app*, unsigned int) ()
#2  0x0000000000c24be4 in smt::mam_impl::add_pattern(quantifier*, app*) ()
#3  0x000000000094e514 in smt::quantifier_manager::assign_eh(quantifier*) ()
#4  0x000000000091d448 in smt::context::propagate_atoms() ()
#5  0x000000000091d6d0 in smt::context::propagate() ()
#6  0x0000000000920e94 in smt::context::push() ()
#7  0x0000000000e7724c in cmd_context::push() ()
#8  0x0000000000e7742c in cmd_context::push(unsigned int) ()
#9  0x0000000000e45210 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) ()
#10 0x000000000043dee0 in read_smtlib2_commands(char const*) ()
#11 0x0000000000428344 in main ()

See also #2828
See also #2332

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant