forked from Z3Prover/z3
-
Notifications
You must be signed in to change notification settings - Fork 3
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
Segfault inside IUC solver #2
Comments
hgvk94
pushed a commit
that referenced
this issue
Aug 4, 2023
…junctions (Z3Prover#6779) After introducing the rewriter.sort_disjunctions option (Z3Prover#6774), I noticed a segfault in a Z3 run that was working fine for me before the PR. I traced the difference to a slight discrepancy between the first patch I submitted and the one we ended up merging: my first version would skip sorting the disjuncts in mk_nflat_core, but still return BR_DONE, while the patch in master returns BR_FAILED instead. This patch fixes that problem, and it makes slightly more sense to me to return a BR_DONE since, if `s` is true, some disjunct (e.g. a `false` or a repeat) might have been simplified away. However I don't fully understand this code. ... and I can't say I understand why the segfault happens. Perhaps that is a separate issue? This is the file to reproduce: https://gist.github.com/mtzguido/b7360c74d3d2e42d89f1bd9149ad26f6 Here's a stack trace of the failure, mk_nflat_or_core is not involved. ``` (gdb) where #0 0x0000555555b98497 in smt::context::get_lit_assignment(unsigned int) const () #1 0x0000555555b984cb in smt::context::get_assignment(sat::literal) const () #2 0x0000555555b98504 in smt::context::get_assignment(unsigned int) const () #3 0x0000555555ca83b8 in smt::context::get_assignment_core(expr*) const () #4 0x0000555555c9af5a in smt::context::get_assignment(expr*) const () #5 0x0000555555d7bd1d in (anonymous namespace)::has_child_assigned_to(smt::context&, app*, lbool, expr*&, unsigned int) () #6 0x0000555555d7c413 in (anonymous namespace)::rel_case_split_queue::next_case_split_core(ptr_vector<expr>&, unsigned int&, unsigned int&, lbool&) () #7 0x0000555555d7c589 in (anonymous namespace)::rel_case_split_queue::next_case_split(unsigned int&, lbool&) () #8 0x0000555555c9c1b7 in smt::context::decide() () #9 0x0000555555ca39fd in smt::context::bounded_search() () #10 0x0000555555ca30c2 in smt::context::search() () Z3Prover#11 0x0000555555ca273d in smt::context::check(unsigned int, expr* const*, bool) () Z3Prover#12 0x0000555555cb166a in smt::kernel::check(unsigned int, expr* const*) () Z3Prover#13 0x0000555555cb9695 in (anonymous namespace)::smt_solver::check_sat_core2(unsigned int, expr* const*) () Z3Prover#14 0x00005555560dc0c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) () Z3Prover#15 0x00005555560d73f3 in combined_solver::check_sat_core(unsigned int, expr* const*) () Z3Prover#16 0x00005555560d34e3 in solver::check_sat(unsigned int, expr* const*) () Z3Prover#17 0x0000555556097b26 in cmd_context::check_sat(unsigned int, expr* const*) () Z3Prover#18 0x0000555556082ff0 in smt2::parser::parse_check_sat() () Z3Prover#19 0x0000555556084dc0 in smt2::parser::parse_cmd() () Z3Prover#20 0x00005555560861b6 in smt2::parser::operator()() () Z3Prover#21 0x00005555560757e6 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) () Z3Prover#22 0x00005555555e8f68 in read_smtlib2_commands(char const*) () Z3Prover#23 0x00005555555ee6f6 in main () (gdb) ```
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Spacer segfaults in the following configuration in release mode
fp.spacer.use_sage=false fp.xform.slice=true fp.spacer.global=true fp.spacer.concretize=true fp.spacer.conjecture=true fp.xform.inline_linear=true fp.xform.inline_eager=true fp.xform.tail_simplifier_pve=false fp.engine=spacer fp.print_statistics=true fp.spacer.elim_aux=true fp.spacer.reach_dnf=true fp.spacer.iuc=1 fp.spacer.iuc.arith=1 fp.validate=true fp.spacer.ground_pobs=true fp.spacer.mbqi=false fp.spacer.iuc.print_farkas_stats=false fp.spacer.iuc.old_hyp_reducer=false fp.spacer.ctp=true fp.spacer.native_mbp=true fp.spacer.use_iuc=true fp.spacer.expand_bnd=false
The issue is that the following assertion at
spacer_proof_utils.cpp:287
is violatedSASSERT(num_params == parents.size() + 1 /* one param is missing */);
stack trace:
` thread #1, name = 'z3', stop reason = signal SIGSEGV: invalid address (fault address: 0x300000002)
spacer::mk_fk_from_ab(ast_manager&, ptr_buffer<app, 16u> const&, unsigned int, parameter const*) + 460 frame #1: 0x00000000013b5594 z3
spacer::theory_axiom_reducer::reduce(app*) + 7444frame Segfault inside IUC solver #2: 0x00000000013a9fc1 z3
spacer::iuc_solver::get_iuc(ref_vector<expr, ast_manager>&) + 3873 frame #3: 0x0000000001380eb7 z3
spacer::prop_solver::internal_check_assumptions(ref_vector<expr, ast_manager>&, ref_vector<expr, ast_manager>&, vector<ref_vector<expr, ast_manager>, true, unsigned int> const&) + 1431frame Spacer assertion violation: File: src/muz/spacer/spacer_context.cpp Line: 950 !lemma->is_ground() || spacer::is_clause(m, l) #4: 0x0000000001382949 z3
spacer::prop_solver::check_assumptions(ref_vector<expr, ast_manager> const&, ref_vector<expr, ast_manager>&, ref_vector<expr, ast_manager> const&, unsigned int, expr* const*, unsigned int) + 505 frame #5: 0x00000000013528bc z3
spacer::pred_transformer::is_reachable(spacer::pob&, ref_vector<expr, ast_manager>, ref, unsigned int&, bool&, datalog::rule const*&, vector<bool, true, unsigned int>&, unsigned int&, bool) + 540frame issue with slicing #6: 0x0000000001361af2 z3
spacer::context::expand_pob(spacer::pob&, sref_buffer<spacer::pob, 16u>&) + 498 frame #7: 0x0000000001363911 z3
spacer::context::check_reachability() + 1345frame failed to produce IUC #8: 0x0000000001365449 z3
spacer::context::solve_core(unsigned int) + 313 frame #9: 0x0000000001365a05 z3
spacer::context::solve(unsigned int) + 197frame MBP reports error "could not evaluate Boolean in model" #10: 0x000000000136e1f2 z3
spacer::dl_interface::query(expr*) + 2818 frame #11: 0x000000000146228f z3
horn_tactic::imp::operator()(ref const&, sref_buffer<goal, 16u>&) + 3455frame Cleanup: avoid defining reserved identifiers Z3Prover/z3#12: 0x00000000009b5e7e z3
cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) + 14 frame #13: 0x00000000009be604 z3
exec(tactic&, ref const&, sref_buffer<goal, 16u>&) + 52frame FP to real and back conversions don't seem to be operational Z3Prover/z3#14: 0x00000000009beba4 z3
check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) + 260 frame #15: 0x0000000000ad4aa6 z3
(anonymous namespace)::tactic2solver::check_sat_core(unsigned int, expr* const*) + 742frame Enabled test for OpenMP in Windows (for old and express versions of visu... Z3Prover/z3#16: 0x0000000000ac6b46 z3
solver_na2as::check_sat(unsigned int, expr* const*) + 166 frame #17: 0x0000000000aaaef6 z3
combined_solver::check_sat(unsigned int, expr* const*) + 1190frame Bugfix for mpf is_normal. Z3Prover/z3#18: 0x0000000000bb7ecd z3
cmd_context::check_sat(unsigned int, expr* const*) + 877 frame #19: 0x0000000000bf7dde z3
smt2::parser::operator()() + 734frame InterpolationContext in InterpolationContext.cs is not public Z3Prover/z3#20: 0x0000000000be37e0 z3
parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) + 64 frame #21: 0x000000000159bdb6 z3
read_smtlib2_commands(char const*) + 534frame sorts inhabited by default? Z3Prover/z3#22: 0x0000000000419212 z3
main + 274 frame #23: 0x0000000001684c79 z3
__libc_start_main + 777frame Static analysis cleanup and open issues Z3Prover/z3#24: 0x000000000041c2ca z3
_start + 42
instance
commit 5f3503c73e9e37ae78d63383bcd063d911b10036
The text was updated successfully, but these errors were encountered: