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
[716] % z3 small.smt2 (error "line 3 column 35: invalid expression, unexpected ')'") (error "line 4 column 27: invalid expression, unexpected ')'") ASSERTION VIOLATION File: ../src/ast/recfun_decl_plugin.h Line: 240 m_plugin->has_def(f) (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [717] % [717] % z3release small.smt2 (error "line 3 column 35: invalid expression, unexpected ')'") (error "line 4 column 27: invalid expression, unexpected ')'") Segmentation fault [718] % [718] % z3san small.smt2 (error "line 3 column 35: invalid expression, unexpected ')'") (error "line 4 column 27: invalid expression, unexpected ')'") ASAN:DEADLYSIGNAL ================================================================= ==25940==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000008 (pc 0x564f44a40f73 bp 0x7fff24a0d540 sp 0x7fff24a0d210 T0) ==25940==The signal is caused by a READ memory access. ==25940==Hint: address points to the zero page. #0 0x564f44a40f72 in recfun::decl::plugin::get_def(func_decl*) ../src/ast/recfun_decl_plugin.h:192 #1 0x564f44a40f72 in recfun::util::get_def(func_decl*) ../src/ast/recfun_decl_plugin.h:241 #2 0x564f44a40f72 in recfun_rewriter::mk_app_core(func_decl*, unsigned int, expr* const*, obj_ref<expr, ast_manager>&) ../src/ast/rewriter/recfun_rewriter.cpp:29 #3 0x564f44a145b3 in reduce_app_core ../src/ast/rewriter/th_rewriter.cpp:225 #4 0x564f44a145b3 in reduce_app ../src/ast/rewriter/th_rewriter.cpp:620 #5 0x564f44a1de6a in process_app<false> ../src/ast/rewriter/rewriter_def.h:298 #6 0x564f44a1de6a in resume_core<false> ../src/ast/rewriter/rewriter_def.h:769 #7 0x564f44a2deba in main_loop<false> ../src/ast/rewriter/rewriter_def.h:728 #8 0x564f44a2deba in operator() ../src/ast/rewriter/rewriter_def.h:800 #9 0x564f44a2deba in th_rewriter::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ../src/ast/rewriter/th_rewriter.cpp:860 #10 0x564f433c8abb in asserted_formulas::assert_expr(expr*, app*) ../src/smt/asserted_formulas.cpp:158 #11 0x564f42eb7b80 in smt::context::assert_expr_core(expr*, app*) ../src/smt/smt_context.cpp:2901 #12 0x564f42eb7b80 in smt::context::assert_expr(expr*, app*) ../src/smt/smt_context.cpp:2913 #13 0x564f42eb7b80 in smt::context::assert_expr(expr*) ../src/smt/smt_context.cpp:2908 #14 0x564f42eb7b80 in smt::context::copy(smt::context&, smt::context&, bool) ../src/smt/smt_context.cpp:178 #15 0x564f435450d9 in smt::parallel::operator()(ref_vector<expr, ast_manager> const&) ../src/smt/smt_parallel.cpp:74 #16 0x564f42ec9613 in smt::context::setup_and_check(bool) ../src/smt/smt_context.cpp:3414 #17 0x564f42d4b83f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/smt/tactic/smt_tactic.cpp:201 #18 0x564f447db4e7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #19 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #20 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #21 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #22 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #23 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #24 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #25 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #26 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #27 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #28 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #29 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #30 0x564f447cde41 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:1034 #31 0x564f447db4e7 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:120 #32 0x564f4473ceda in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:148 #33 0x564f4473f1dd 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 #34 0x564f4463db38 in check_sat_core2 ../src/solver/tactic2solver.cpp:185 #35 0x564f44644ef7 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67 #36 0x564f44602904 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:246 #37 0x564f445e39f1 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:330 #38 0x564f4453ea60 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1549 #39 0x564f44485663 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596 #40 0x564f44485663 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938 #41 0x564f44485663 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130 #42 0x564f4443cb85 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179 #43 0x564f41ace886 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:89 #44 0x564f41aa70be in main ../src/shell/main.cpp:352 #45 0x7fb589f26b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96) #46 0x564f41abaef9 in _start (/home/suz/software/z3san/build-04272020171048-38e0968/z3+0x1f7ef9) AddressSanitizer can not provide additional info. SUMMARY: AddressSanitizer: SEGV ../src/ast/recfun_decl_plugin.h:192 in recfun::decl::plugin::get_def(func_decl*) ==25940==ABORTING [719] % [719] % cat small.smt2 (set-option :smt.threads 2) (declare-datatypes ((a 0)) (((b (c a)) (d)))) (define-fun-rec app ((e a) (h a)) a) (define-fun-rec f ((g a)) a) (assert (forall ((i a) (j a)) (= (f (app i j)) j))) (assert (not (forall ((k a)) (= (f (f k)) k)))) (check-sat) [720] %
OS: Ubuntu 18.04 Commit: b571e43
The text was updated successfully, but these errors were encountered:
fa1197a
No branches or pull requests
OS: Ubuntu 18.04
Commit: b571e43
The text was updated successfully, but these errors were encountered: