Closed 5hadowblad3 closed 4 years ago
Hi, there.
There is a segmentation fault using z3.
To reproduce this issue, simply run z3 poc.smt2 z3-seg-debug-invariant.smt2.zip
OS: Ubuntu 16.06 commit 37bc4a44
Here is the trace reported by ASAN.
ASAN:SIGSEGV ================================================================= ==15814==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x000001e424c3 bp 0x7fffff3ddb70 sp 0x7fffff3ddb40 T0) #0 0x1e424c2 in nla::emonics::invariant() const::{lambda(unsigned int, unsigned int)#1}::operator()(unsigned int, unsigned int) const (/home/heqing/dependence/z3-debug/build/z3+0x1e424c2) #1 0x1e438f0 in _M_invoke /usr/include/c++/5/functional:1857 #2 0x1e4719c in std::function<bool (unsigned int, unsigned int)>::operator()(unsigned int, unsigned int) const (/home/heqing/dependence/z3-debug/build/z3+0x1e4719c) #3 0x1e431f9 in nla::emonics::invariant() const ../src/math/lp/emonics.cpp:573 #4 0x1e40a99 in nla::emonics::add(unsigned int, unsigned int, unsigned int const*) ../src/math/lp/emonics.cpp:346 #5 0x1e23fba in nla::emonics::add(unsigned int, old_svector<unsigned int, unsigned int> const&) ../src/math/lp/emonics.h:158 #6 0x1e0d128 in nla::core::add_monic(unsigned int, unsigned int, unsigned int const*) ../src/math/lp/nla_core.cpp:132 #7 0x1d53d08 in nla::solver::add_monic(unsigned int, unsigned int, unsigned int const*) ../src/math/lp/nla_solver.cpp:30 #8 0xdb0cf9 in smt::theory_lra::imp::switcher::add_monic(unsigned int, unsigned int, unsigned int const*) ../src/smt/theory_lra.cpp:313 #9 0xdb5150 in smt::theory_lra::imp::internalize_mul(app*) ../src/smt/theory_lra.cpp:700 #10 0xdb3c67 in smt::theory_lra::imp::linearize(smt::theory_lra::imp::scoped_internalize_state&) ../src/smt/theory_lra.cpp:570 #11 0xdb351e in smt::theory_lra::imp::linearize_term(expr*, smt::theory_lra::imp::scoped_internalize_state&) ../src/smt/theory_lra.cpp:525 #12 0xdb6d43 in smt::theory_lra::imp::internalize_def(app*) ../src/smt/theory_lra.cpp:944 #13 0xdb95c6 in smt::theory_lra::imp::internalize_term(app*) (/home/heqing/dependence/z3-debug/build/z3+0xdb95c6) #14 0xdaa2f3 in smt::theory_lra::internalize_term(app*) ../src/smt/theory_lra.cpp:3857 #15 0x1109a23 in smt::context::internalize_theory_term(app*) ../src/smt/smt_internalizer.cpp:834 #16 0x1108bf9 in smt::context::internalize_term(app*) ../src/smt/smt_internalizer.cpp:773 #17 0x1104bd3 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:358 #18 0x1107ec5 in smt::context::internalize_formula_core(app*, bool) ../src/smt/smt_internalizer.cpp:587 #19 0x11058d8 in smt::context::internalize_eq(app*, bool) ../src/smt/smt_internalizer.cpp:426 #20 0x1105539 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:408 #21 0x1104ae3 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350 #22 0x1107ec5 in smt::context::internalize_formula_core(app*, bool) ../src/smt/smt_internalizer.cpp:587 #23 0x1105649 in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:416 #24 0x1104ae3 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350 #25 0x1104fdb in smt::context::internalize_formula(expr*, bool) ../src/smt/smt_internalizer.cpp:374 #26 0x1104ae3 in smt::context::internalize_rec(expr*, bool) ../src/smt/smt_internalizer.cpp:350 #27 0x1103022 in smt::context::internalize_assertion(expr*, app*, unsigned int) ../src/smt/smt_internalizer.cpp:234 #28 0xceafb7 in smt::context::internalize_instance(expr*, app*, unsigned int) ../src/smt/smt_context.h:1588 #29 0xce7a48 in smt::qi_queue::instantiate(smt::qi_queue::entry&) ../src/smt/qi_queue.cpp:282 #30 0xce9bb4 in smt::qi_queue::final_check_eh() ../src/smt/qi_queue.cpp:395 #31 0xcdc2b2 in smt::quantifier_manager::imp::final_check_eh(bool) ../src/smt/smt_quantifier.cpp:366 #32 0xcd8a2a in smt::quantifier_manager::final_check_eh(bool) ../src/smt/smt_quantifier.cpp:460 #33 0x11bf8d8 in smt::context::final_check() ../src/smt/smt_context.cpp:3911 #34 0x11be6e0 in smt::context::bounded_search() ../src/smt/smt_context.cpp:3819 #35 0x11bbe1b in smt::context::search() ../src/smt/smt_context.cpp:3646 #36 0x11ba3a3 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3531 #37 0x1126e64 in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116 #38 0x1125b45 in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:296 #39 0xc51040 in ctx_solver_simplify_tactic::simplify_bool(expr*, obj_ref<expr, ast_manager>&) ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:249 #40 0xc503f5 in ctx_solver_simplify_tactic::reduce(obj_ref<expr, ast_manager>&) ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:179 #41 0xc4ed4e in ctx_solver_simplify_tactic::reduce(goal&) ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:95 #42 0xc4e989 in ctx_solver_simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/ctx_solver_simplify_tactic.cpp:72 #43 0x19e46d5 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:909 #44 0x19dd4a2 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111 #45 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #46 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #47 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #48 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #49 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #50 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #51 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #52 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #53 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #54 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #55 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #56 0x19dd5f1 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #57 0x19e30e3 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:763 #58 0x1a127ce in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148 #59 0x1a12c69 in 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> >&) ../src/tactic/tactic.cpp:168 #60 0x192140c in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223 #61 0x18c6465 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895 #62 0x18c6c76 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001 #63 0x18c8051 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130 #64 0x18a7036 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179 #65 0x41f02b in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89 #66 0x415b1e in main ../src/shell/main.cpp:352 #67 0x7f8d905af82f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2082f) #68 0x414888 in _start (/home/heqing/dependence/z3-debug/build/z3+0x414888) AddressSanitizer can not provide additional info. SUMMARY: AddressSanitizer: SEGV ??:0 nla::emonics::invariant() const::{lambda(unsigned int, unsigned int)#1}::operator()(unsigned int, unsigned int) const ==15814==ABORTING
doesn't repro
NikolajBjorner
commented
4 years ago NikolajBjorner
commented
4 years ago
Hi, there.
There is a segmentation fault using z3.
To reproduce this issue, simply run z3 poc.smt2 z3-seg-debug-invariant.smt2.zip
OS: Ubuntu 16.06 commit 37bc4a44
Here is the trace reported by ASAN.