[523] % z3release smt.threads=2 small.smt2 
Segmentation fault
[524] % z3debug smt.threads=2 small.smt2 
Segmentation fault
[525] % z3san smt.threads=2 small.smt2 
ASAN:DEADLYSIGNAL
=================================================================
==15035==ERROR: AddressSanitizer: stack-overflow on address 0x7ffe7399dff0 (pc 0x564a89d3fc94 bp 0x7ffe7399e230 sp 0x7ffe7399dfc0 T0)
    #0 0x564a89d3fc93 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2153
    #1 0x564a89d2fe88 in ast_manager::mk_app(func_decl*, unsigned int, expr* const*) ../src/ast/ast.cpp:2273
    #2 0x564a88a71d98 in ast_manager::mk_app(func_decl*, ref_vector<expr, ast_manager> const&) ../src/ast/ast.h:1824
    #3 0x564a88a71d98 in datatype_factory::get_fresh_value(sort*) ../src/model/datatype_factory.cpp:177
    #4 0x564a879e8f85 in proto_model::get_fresh_value(sort*) ../src/smt/proto_model/proto_model.cpp:324
    #5 0x564a889f2fc8 in array_factory::get_fresh_value(sort*) ../src/model/array_factory.cpp:135
    #6 0x564a879e8f85 in proto_model::get_fresh_value(sort*) ../src/smt/proto_model/proto_model.cpp:324
    #7 0x564a88a7197c in datatype_factory::get_fresh_value(sort*) ../src/model/datatype_factory.cpp:166
...
SUMMARY: AddressSanitizer: stack-overflow ../src/ast/ast.cpp:2153 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*)
==15035==ABORTING
[526] % 
[526] % cat small.smt2 
(declare-datatypes ((a 0)) (((f) (g (e (Array Int a))))))
(declare-fun b () a)
(declare-fun c () a)
(declare-fun d () a)
(assert (distinct b c d))
(check-sat)
[527] %