[551] % z3release small.smt2
Segmentation fault
[552] % z3san small.smt2
ASAN:DEADLYSIGNAL
=================================================================
==7134==ERROR: AddressSanitizer: stack-overflow on address 0x7ffe5f155ca0 (pc 0x56474539b62e bp 0x7ffe5f1565e0 sp 0x7ffe5f155c80 T0)
    #0 0x56474539b62d in static_features::update_core(expr*) ../src/ast/static_features.cpp:170
    #1 0x5647453a592e in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:415
    #2 0x5647453a5f14 in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:452
    #3 0x5647453a5f14 in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:452
    #4 0x5647453a5f14 in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:452
    #5 0x5647453a5f14 in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:452
    #6 0x5647453a5f14 in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:452
    #7 0x5647453a5f14 in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:452
    #8 0x5647453a5f14 in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:452
    #9 0x5647453a5f14 in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:452
    #10 0x5647453a5f14 in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:452
    #11 0x5647453a779e in static_features::process(expr*, bool, bool, bool, unsigned int) ../src/ast/static_features.cpp:411
...
SUMMARY: AddressSanitizer: stack-overflow ../src/ast/static_features.cpp:170 in static_features::update_core(expr*)
==7134==ABORTING
[553] % 
[553] % cat small.smt2
(declare-fun a () String)
(define-fun b () String (str.++ a a a))
(define-fun c () String (str.replace_all b "A" b))
(define-fun d () String (str.replace_all c "A" c))
(assert (= a (str.replace_all (str.++ d d) (ite (= a "A") "A" "") (str.++ d d))))
(check-sat)
[554] %