search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Segment fault at ast.h:504 (smt.core.minimize true + fp.xform.fix_unbound_vars ) #3817

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula

(set-logic HORN)
(set-option :smt.core.minimize true)
(set-option :fp.xform.fix_unbound_vars true)
(assert (forall ((q7 (_ BitVec 10)) (q8 (_ BitVec 10)) (q9 (_ BitVec 10)) (q10 (_ BitVec 12))) true))
(assert (forall ((q11 (_ BitVec 10)) (q12 (_ BitVec 10)) (q13 (_ BitVec 10)) (q14 Bool)) q14))
(check-sat)

z3 3313590 throw a seg fault

================================================================
==30194==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000004 (pc 0x000000472ba9 bp 0x7ffd58468fa0 sp 0x7ffd58468f90 T0)
==30194==The signal is caused by a READ memory access.
==30194==Hint: address points to the zero page.
    #0 0x472ba8 in ast::get_kind() const ../src/ast/ast.h:504
    #1 0x4d20a9 in is_decl(ast const*) ../src/ast/ast.h:910
    #2 0x27f7a42 in ast_mark::is_marked(ast*) const ../src/ast/ast.cpp:3462
    #3 0x1dd0c86 in proof_post_order::next() ../src/ast/proofs/proof_utils.cpp:42
    #4 0x8515a9 in spacer::theory_axiom_reducer::reduce(app*) ../src/muz/spacer/spacer_proof_utils.cpp:361
    #5 0x847c89 in spacer::iuc_solver::get_iuc(ref_vector<expr, ast_manager>&) ../src/muz/spacer/spacer_iuc_solver.cpp:339
    #6 0x833236 in spacer::prop_solver::internal_check_assumptions(ref_vector<expr, ast_manager>&, ref_vector<expr, ast_manager>&, old_vector<r
ef_vector<expr, ast_manager>, true, unsigned int> const&) ../src/muz/spacer/spacer_prop_solver.cpp:336
    #7 0x833bc1 in 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) ../src/muz/spacer/spacer_prop_solver.cpp:385
    #8 0x7a9d93 in spacer::pred_transformer::is_reachable(spacer::pob&, ref_vector<expr, ast_manager>*, ref<model>*, unsigned int&, bool&, data
log::rule const*&, old_svector<bool, unsigned int>&, unsigned int&) ../src/muz/spacer/spacer_context.cpp:1387
    #9 0x7c899e in spacer::context::expand_pob(spacer::pob&, sref_buffer<spacer::pob, 16u>&) ../src/muz/spacer/spacer_context.cpp:3378
    #10 0x7c6189 in spacer::context::check_reachability() ../src/muz/spacer/spacer_context.cpp:3180
    #11 0x7c31f6 in spacer::context::solve_core(unsigned int) ../src/muz/spacer/spacer_context.cpp:2999
    #12 0x7bf2c4 in spacer::context::solve(unsigned int) ../src/muz/spacer/spacer_context.cpp:2695
    #13 0x74b228 in spacer::dl_interface::query(expr*) ../src/muz/spacer/spacer_dl_interface.cpp:167
    #14 0xb18f35 in datalog::context::query(expr*) ../src/muz/base/dl_context.cpp:876
    #15 0x69e48a in horn_tactic::imp::verify(expr*, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&) ..
/src/muz/fp/horn_tactic.cpp:254
    #16 0x69e02a in horn_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/muz/fp/horn_tactic.cpp:239
    #17 0x69f9d3 in horn_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/muz/fp/horn_tactic.cpp:384
    #18 0x1e4c8e7 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:915
    #19 0x1e3aabb in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148
    #20 0x1e3b049 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manage
r::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) ../src
/tactic/tactic.cpp:168
    #21 0x1dc3940 in check_sat_core2 ../src/solver/tactic2solver.cpp:185
    #22 0x1dc125b in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #23 0x1dbba8d in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246
    #24 0x1db8803 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330
    #25 0x1d67adc in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1581
    #26 0x1ce5ad9 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #27 0x1ce9f32 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #28 0x1ceb73f in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #29 0x1cc56c6 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:
3179
    #30 0x46f791 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89
    #31 0x459a9c in main ../src/shell/main.cpp:352
    #32 0x7f3737e3f82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f)
rainoftime commented 4 years ago

Thre are many segfaults ending at ast.h:504, but have different stack traces.

NikolajBjorner commented 4 years ago

fixed by some other bug fix