We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
[520] % z3san small.smt2 ================================================================= ==2913==ERROR: AddressSanitizer: heap-use-after-free on address 0x6120000c3f4c at pc 0x556a1973569e bp 0x7ffe6f9a9680 sp 0x7ffe6f9a9670 READ of size 4 at 0x6120000c3f4c thread T0 #0 0x556a1973569d in obj_hash_entry<expr>::get_hash() const ../src/util/obj_hashtable.h:35 #1 0x556a1973569d in core_hashtable<obj_hash_entry<expr>, obj_ptr_hash<expr>, ptr_eq<expr> >::find_core(expr* const&) const ../src/util/hashtable.h:516 #2 0x556a1973569d in core_hashtable<obj_hash_entry<expr>, obj_ptr_hash<expr>, ptr_eq<expr> >::contains(expr* const&) const ../src/util/hashtable.h:531 #3 0x556a1973569d in expr_sparse_mark::is_marked(expr*) const ../src/ast/ast.h:2467 #4 0x556a1973569d in euf::arith_extract_eq::solve_mul(expr*, expr*, expr*, dependency_manager<ast_manager::expr_dependency_config>::dependency*, vector<euf::dependent_eq, true, unsigned int>&) ../src/ast/simplifiers/extract_eqs.cpp:201 #5 0x556a1973569d in euf::arith_extract_eq::solve_eq(expr*, expr*, expr*, dependency_manager<ast_manager::expr_dependency_config>::dependency*, vector<euf::dependent_eq, true, unsigned int>&) ../src/ast/simplifiers/extract_eqs.cpp:239 #6 0x556a19735d9d in euf::arith_extract_eq::get_eqs(dependent_expr const&, vector<euf::dependent_eq, true, unsigned int>&) ../src/ast/simplifiers/extract_eqs.cpp:252 #7 0x556a196b2521 in euf::solve_eqs::get_eqs(vector<euf::dependent_eq, true, unsigned int>&) ../src/ast/simplifiers/solve_eqs.cpp:56 #8 0x556a196c97bd in euf::solve_eqs::reduce() ../src/ast/simplifiers/solve_eqs.cpp:236 #9 0x556a165c2a80 in dependent_expr_state_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/dependent_expr_state_tactic.h:112 #10 0x556a19678a91 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:113 #11 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #12 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #13 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #14 0x556a1966d3f7 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1057 #15 0x556a19673827 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:342 #16 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #17 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #18 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #19 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #20 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #21 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #22 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #23 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #24 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #25 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #26 0x556a19640cc4 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:165 #27 0x556a196426e4 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:185 #28 0x556a1959dea8 in check_sat_core2 ../src/solver/tactic2solver.cpp:233 #29 0x556a195c275f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67 #30 0x556a195dc5b4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:253 #31 0x556a195af1e6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318 #32 0x556a19526ac5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1700 #33 0x556a1947eef3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611 #34 0x556a1947eef3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953 #35 0x556a1947eef3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3166 #36 0x556a19434055 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3217 #37 0x556a1656b651 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:147 #38 0x556a1653f241 in main ../src/shell/main.cpp:382 #39 0x7fe5445bfc86 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21c86) #40 0x556a1654c2f9 in _start (/local/suz-local/software/z3san/build-12272022201939-7cc58c9/z3+0x20b2f9) 0x6120000c3f4c is located 12 bytes inside of 260-byte region [0x6120000c3f40,0x6120000c4044) freed by thread T0 here: #0 0x7fe5455cb7a8 in __interceptor_free (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xde7a8) #1 0x556a1b3ba854 in memory::deallocate(void*) ../src/util/memory_manager.cpp:286 #2 0x556a1adead03 in ast_manager::deallocate_node(ast*, unsigned int) ../src/ast/ast.h:1691 #3 0x556a1adead03 in ast_manager::delete_node(ast*) ../src/ast/ast.cpp:1918 #4 0x556a196c959b in ast_manager::dec_ref(ast*) ../src/ast/ast.h:1650 #5 0x556a196c959b in dependent_expr::~dependent_expr() ../src/ast/simplifiers/dependent_expr.h:88 #6 0x556a196c959b in void std::_Destroy<dependent_expr>(dependent_expr*) /usr/include/c++/7/bits/stl_construct.h:98 #7 0x556a196c959b in dependent_expr* std::_Destroy_n_aux<false>::__destroy_n<dependent_expr*, unsigned int>(dependent_expr*, unsigned int) /usr/include/c++/7/bits/stl_construct.h:148 #8 0x556a196c959b in dependent_expr* std::_Destroy_n<dependent_expr*, unsigned int>(dependent_expr*, unsigned int) /usr/include/c++/7/bits/stl_construct.h:182 #9 0x556a196c959b in dependent_expr* std::destroy_n<dependent_expr*, unsigned int>(dependent_expr*, unsigned int) /usr/include/c++/7/bits/stl_construct.h:228 #10 0x556a196c959b in vector<dependent_expr, true, unsigned int>::destroy_elements() ../src/util/vector.h:169 #11 0x556a196c959b in vector<dependent_expr, true, unsigned int>::reset() ../src/util/vector.h:388 #12 0x556a196c959b in euf::solve_eqs::reduce() ../src/ast/simplifiers/solve_eqs.cpp:233 #13 0x556a165c2a80 in dependent_expr_state_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/dependent_expr_state_tactic.h:112 #14 0x556a19678a91 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:113 #15 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #16 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #17 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #18 0x556a1966d3f7 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1057 #19 0x556a19673827 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:342 #20 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #21 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #22 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #23 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #24 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #25 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #26 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #27 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #28 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #29 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #30 0x556a19640cc4 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:165 #31 0x556a196426e4 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:185 #32 0x556a1959dea8 in check_sat_core2 ../src/solver/tactic2solver.cpp:233 #33 0x556a195c275f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67 #34 0x556a195dc5b4 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:253 #35 0x556a195af1e6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:318 #36 0x556a19526ac5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1700 #37 0x556a1947eef3 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2611 #38 0x556a1947eef3 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2953 #39 0x556a1947eef3 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3166 #40 0x556a19434055 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3217 previously allocated by thread T0 here: #0 0x7fe5455cbb40 in __interceptor_malloc (/usr/lib/x86_64-linux-gnu/libasan.so.4+0xdeb40) #1 0x556a1b3baa7d in memory::allocate(unsigned long) ../src/util/memory_manager.cpp:301 #2 0x556a1ae11066 in ast_manager::allocate_node(unsigned int) ../src/ast/ast.h:1687 #3 0x556a1ae11066 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2170 #4 0x556a1ae000c5 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2288 #5 0x556a1ae0f32a in ast_manager::mk_app(int, int, unsigned int, parameter const*, unsigned int, expr* const*, sort*) ../src/ast/ast.cpp:1950 #6 0x556a1ae0f32a in ast_manager::mk_app(int, int, unsigned int, expr* const*) ../src/ast/ast.cpp:1955 #7 0x556a1ac0b450 in arith_util::mk_add(unsigned int, expr* const*) const ../src/ast/arith_decl_plugin.h:445 #8 0x556a1ac0b450 in expr2polynomial::imp::to_expr(obj_ref<polynomial::polynomial, polynomial::manager> const&, bool, obj_ref<expr, ast_manager>&) ../src/ast/expr2polynomial.cpp:456 #9 0x556a18f2ce6a in factor_tactic::rw_cfg::mk_split_eq(polynomial::manager::factors const&, obj_ref<expr, ast_manager>&) ../src/tactic/arith/factor_tactic.cpp:74 #10 0x556a18f2ce6a in factor_tactic::rw_cfg::factor(func_decl*, expr*, expr*, obj_ref<expr, ast_manager>&) ../src/tactic/arith/factor_tactic.cpp:201 #11 0x556a18f328ed in factor_tactic::rw_cfg::reduce_app(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/tactic/arith/factor_tactic.cpp:230 #12 0x556a18f328ed in void rewriter_tpl<factor_tactic::rw_cfg>::process_app<false>(app*, rewriter_core::frame&) ../src/ast/rewriter/rewriter_def.h:316 #13 0x556a18f33f0d in void rewriter_tpl<factor_tactic::rw_cfg>::resume_core<false>(obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:787 #14 0x556a18f350dd in void rewriter_tpl<factor_tactic::rw_cfg>::main_loop<false>(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:746 #15 0x556a18f360db in factor_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/arith/factor_tactic.cpp:269 #16 0x556a18f360db in factor_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/arith/factor_tactic.cpp:313 #17 0x556a1966c1fc in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1032 #18 0x556a19678a91 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:113 #19 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #20 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #21 0x556a1966d3f7 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1057 #22 0x556a19673827 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:342 #23 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #24 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #25 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #26 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #27 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #28 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #29 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #30 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #31 0x556a1966da41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1153 #32 0x556a196798ba in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:122 #33 0x556a19640cc4 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:165 #34 0x556a196426e4 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:185 #35 0x556a1959dea8 in check_sat_core2 ../src/solver/tactic2solver.cpp:233 SUMMARY: AddressSanitizer: heap-use-after-free ../src/util/obj_hashtable.h:35 in obj_hash_entry<expr>::get_hash() const Shadow bytes around the buggy address: 0x0c2480010790: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd 0x0c24800107a0: fd fd fd fd fd fd fd fd fd fd fa fa fa fa fa fa 0x0c24800107b0: fa fa fa fa fa fa fa fa fd fd fd fd fd fd fd fd 0x0c24800107c0: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd 0x0c24800107d0: fd fd fd fd fd fd fd fd fd fd fa fa fa fa fa fa =>0x0c24800107e0: fa fa fa fa fa fa fa fa fd[fd]fd fd fd fd fd fd 0x0c24800107f0: fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd fd 0x0c2480010800: fd fd fd fd fd fd fd fd fd fa fa fa fa fa fa fa 0x0c2480010810: fa fa fa fa fa fa fa fa 00 00 00 00 00 00 00 00 0x0c2480010820: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 0x0c2480010830: 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 Shadow byte legend (one shadow byte represents 8 application bytes): Addressable: 00 Partially addressable: 01 02 03 04 05 06 07 Heap left redzone: fa Freed heap region: fd Stack left redzone: f1 Stack mid redzone: f2 Stack right redzone: f3 Stack after return: f5 Stack use after scope: f8 Global redzone: f9 Global init order: f6 Poisoned by user: f7 Container overflow: fc Array cookie: ac Intra object redzone: bb ASan internal: fe Left alloca redzone: ca Right alloca redzone: cb ==2913==ABORTING [521] % [521] % cat small.smt2 (declare-fun a () Real) (declare-fun b () Real) (declare-fun c () Real) (declare-fun d () Real) (declare-fun e () Real) (declare-fun f () Real) (declare-fun g () Real) (declare-fun h () Real) (declare-fun i () Real) (declare-fun j () Real) (declare-fun k () Real) (declare-fun l () Real) (declare-fun m () Real) (declare-fun n () Real) (declare-fun o () Real) (assert (= (* i o) (* m j) h)) (assert (= (+ g k o) 0)) (assert (distinct (* h a b) a)) (assert (= h (- d b))) (assert (= (- c n l) e g)) (assert (= j c (+ d (* e f)))) (assert (> o 0)) (check-sat)
The text was updated successfully, but these errors were encountered:
07ab4d3
fix #6513
293627c
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
fix Z3Prover#6513
81e77fb
100c733
No branches or pull requests
The text was updated successfully, but these errors were encountered: