(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert (distinct (str.substr a 3 (str.len b)) ""))
(assert (distinct
         (ite (= (str.len (str.substr (str.replace a b "") 0 (- (str.len c)))) 1) 0 2)
         (ite (= (str.at (str.replace a b "") 2) "") 1 2)))
(check-sat)
(get-model)

(model 
  (define-fun b () String
    "\x00")
  (define-fun a () String
    "\x00\x00\x00\x00\x00")
  (define-fun c () String
    "\x00")
)