[518] % z3debug tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[519] % z3release tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
Segmentation fault
[520] % z3san tactic.default_tactic=smt sat.euf=true model_validate=true small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==21324==ERROR: AddressSanitizer: SEGV on unknown address 0x000000001012 (pc 0x564e88cd99b1 bp 0x7fff10ce6180 sp 0x7fff10ce5f80 T0)
==21324==The signal is caused by a READ memory access.
    #0 0x564e88cd99b0 in euf::enode::hash() const ../src/ast/euf/euf_enode.h:167
    #1 0x564e88cd99b0 in obj_map<euf::enode, euf::enode*>::key_data::hash() const ../src/util/obj_hashtable.h:77
    #2 0x564e88cd99b0 in obj_map<euf::enode, euf::enode*>::obj_map_entry::get_hash() const ../src/util/obj_hashtable.h:86
    #3 0x564e88cd99b0 in core_hashtable<obj_map<euf::enode, euf::enode*>::obj_map_entry, obj_hash<obj_map<euf::enode, euf::enode*>::key_data>, default_eq<obj_map<euf::enode, euf::enode*>::key_data> >::insert(obj_map<euf::enode, euf::enode*>::key_data&&) ../src/util/hashtable.h:403
    #4 0x564e88cd99b0 in obj_map<euf::enode, euf::enode*>::insert(euf::enode*, euf::enode* const&) ../src/util/obj_hashtable.h:141
    #5 0x564e88cd99b0 in dt::solver::occurs_check_enter(euf::enode*) ../src/sat/smt/dt_solver.cpp:589
    #6 0x564e88cdb477 in dt::solver::occurs_check(euf::enode*) ../src/sat/smt/dt_solver.cpp:637
    #7 0x564e88cdc55c in dt::solver::check() ../src/sat/smt/dt_solver.cpp:667
    #8 0x564e88b1c6ca in euf::solver::check() ../src/sat/smt/euf_solver.cpp:457
    #9 0x564e8a8c52dc in sat::solver::final_check() ../src/sat/sat_solver.cpp:1752
    #10 0x564e8a8ececf in sat::solver::basic_search() ../src/sat/sat_solver.cpp:1727
    #11 0x564e8a8edd01 in sat::solver::bounded_search() ../src/sat/sat_solver.cpp:1714
    #12 0x564e8a8eee1f in sat::solver::check(unsigned int, sat::literal const*) ../src/sat/sat_solver.cpp:1341
    #13 0x564e88b0ba62 in sat_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:66
    #14 0x564e88b0f1c5 in sat_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/sat/tactic/sat_tactic.cpp:202
    #15 0x564e89a033e8 in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactical.cpp:924
    #16 0x564e899cdfce in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ../src/tactic/tactic.cpp:150
    #17 0x564e899cf977 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:170
    #18 0x564e89824730 in check_sat_core2 ../src/solver/tactic2solver.cpp:187
    #19 0x564e89847d2f in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #20 0x564e89860774 in combined_solver::check_sat_core(unsigned int, expr* const*) ../src/solver/combined_solver.cpp:252
    #21 0x564e898356e6 in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:332
    #22 0x564e897b77d5 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1623
    #23 0x564e8970e823 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2605
    #24 0x564e8970e823 in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2947
    #25 0x564e8970e823 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3139
    #26 0x564e896c3f55 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3188
    #27 0x564e86a5396f in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #28 0x564e869fe357 in main ../src/shell/main.cpp:372
    #29 0x7fdab5d54b96 in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x21b96)
    #30 0x564e86a14109 in _start (/local/suz-local/software/z3san/build-04272021214656-30e904b/z3+0x206109)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV ../src/ast/euf/euf_enode.h:167 in euf::enode::hash() const
==21324==ABORTING
[521] % 
[521] % cat small.smt2
(declare-datatypes ((a 0) (b 0) (c 0)) (((d)) ((cons (car c) (cdr b)) (e)) ((f (children b)))))
(declare-fun g () b)
(declare-fun h () b)
(declare-fun i () b)
(assert (or (and (or (or true (and ((_ is cons) (ite ((_ is cons) h) (cdr h) e)))) (distinct (ite ((_ is f) (f g)) (children (f g)) e) i)))))
(check-sat)
[522] %