(declare-fun a () String)     
(declare-fun b () String)     
(declare-fun c () String)     
(assert (= (str.substr a 0 (str.len b)) ""))     
(assert (=      
            (ite      
                (= (str.len (str.substr (str.replace (str.replace a b "") "29M8u" "") 1 (- (str.len c) 1))) 0) 1 0
            )      
            0       
        )      
)     
(check-sat)   

Failed to verify: get_length(e, len1)
*** stack smashing detected ***: <unknown> terminated
[1]    65175 abort      z3/build-2019-09-14-69abe16-no_asserts/z3