Assertion violation at src/ast/recfun_decl_plugin.h:240

[wintered]

[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