FStar icon indicating copy to clipboard operation
FStar copied to clipboard

Z3 4.8.5 segfaults on aarch64 linux

Open gebner opened this issue 1 year ago • 0 comments

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

gebner avatar Sep 14 '24 18:09 gebner