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
[529] % z3 small.smt2 ASSERTION VIOLATION File: ../src/util/vector.h Line: 405 !empty() (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [530] % z3release small.smt2 Segmentation fault [531] % z3san small.smt2 ASAN:DEADLYSIGNAL ================================================================= ==28377==ERROR: AddressSanitizer: SEGV on unknown address 0x00017fff7fff (pc 0x55c7832168ed bp 0x7ffdd9dc97c0 sp 0x7ffdd9dc9720 T0) ==28377==The signal is caused by a READ memory access. #0 0x55c7832168ec in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::back() const ../src/util/ref_vector.h:121 #1 0x55c7832168ec in purify_arith_proc::rw_cfg::push_cnstr_pr(app*) ../src/tactic/arith/purify_arith_tactic.cpp:263 #2 0x55c78322dff5 in purify_arith_proc::process_quantifier(quantifier*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/tactic/arith/purify_arith_tactic.cpp:742 #3 0x55c78322ea90 in purify_arith_proc::rw_cfg::get_subst(expr*, expr*&, app*&) ../src/tactic/arith/purify_arith_tactic.cpp:696 #4 0x55c78322ea90 in bool rewriter_tpl<purify_arith_proc::rw_cfg>::visit<true>(expr*, unsigned int) ../src/ast/rewriter/rewriter_def.h:140 #5 0x55c783235074 in void rewriter_tpl<purify_arith_proc::rw_cfg>::main_loop<true>(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:715 #6 0x55c78323a601 in rewriter_tpl<purify_arith_proc::rw_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/rewriter_def.h:798 #7 0x55c78323a601 in purify_arith_proc::operator()(ref<model_converter>&, bool) ../src/tactic/arith/purify_arith_tactic.cpp:761 #8 0x55c783240abd in purify_arith_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/arith/purify_arith_tactic.cpp:908 #9 0x55c783a72f61 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:111 #10 0x55c783a73f57 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #11 0x55c783a73f57 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #12 0x55c7839d594a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148 #13 0x55c7839d7c4d 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 #14 0x55c783787cc0 in check_sat_using_tactict_cmd::execute(cmd_context&) ../src/cmd_context/tactic_cmds.cpp:223 #15 0x55c7837172e8 in smt2::parser::parse_ext_cmd(int, int) ../src/parsers/smt2/smt2parser.cpp:2895 #16 0x55c78371df5c in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:3001 #17 0x55c78371df5c in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130 #18 0x55c7836d55f5 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179 #19 0x55c780d671a6 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89 #20 0x55c780d3fa3e in main ../src/shell/main.cpp:352 #21 0x7f858678eb96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96) #22 0x55c780d53819 in _start (/home/suz/software/z3san/build-04272020120633-8996e81/z3+0x1f7819) AddressSanitizer can not provide additional info. SUMMARY: AddressSanitizer: SEGV ../src/util/ref_vector.h:121 in ref_vector_core<expr, ref_manager_wrapper<expr, ast_manager> >::back() const ==28377==ABORTING [532] % [532] % cat small.smt2 (set-option :proof true) (declare-sort a) (declare-fun f (a) a) (assert (forall ((t a)) (= (f t) t))) (check-sat-using purify-arith) [533] %
OS: Ubuntu 18.04 Commit: 3a63c37
The text was updated successfully, but these errors were encountered:
38e0968
No branches or pull requests
OS: Ubuntu 18.04
Commit: 3a63c37
The text was updated successfully, but these errors were encountered: