(set-logic QF_S)
(declare-fun b () Bool)
(declare-fun f () Bool)
(declare-fun a () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () String)
(declare-fun g () String)
(declare-fun h () String)
(assert (= (= b f) (not (= "" (str.substr a 32 (str.len c))))))
(assert (= b f (= h (str.++ (str.substr a (str.len c) (str.len d)) e)) (= g "")))
(check-sat)

$ z3 test.smt2
Segmentation fault
$ cat test.smt2
(set-logic QF_S)
(declare-fun b () Bool)
(declare-fun f () Bool)
(declare-fun a () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () String)
(declare-fun g () String)
(declare-fun h () String)
(assert (= (= b f) (not (= "" (str.substr a 32 (str.len c))))))
(assert (= b f (= h (str.++ (str.substr a (str.len c) (str.len d)) e)) (= g "")))
(check-sat)