FStar
FStar copied to clipboard
Z3 4.8.5 segfaults on aarch64 linux
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