(declare-fun a () String)
(declare-fun b () Int)
(assert (let ((a!1 (distinct (str.replace "A" (int.to.str b) a)
                     (str.++ "A" (str.replace "" (int.to.str b) a))))
      (a!2 (str.++ (str.replace (str.++ (str.substr a 5 b) (str.substr a b 8))
                                (str.substr a b 9)
                                "")
                   (str.substr a (- b) (str.len a)))))
  (or a!1 (= (str.replace a (str.at a b) "") a!2))))
(check-sat)

NOT IMPLEMENTED YET!
ASSERTION VIOLATION
File: ../src/smt/theory_str.cpp
Line: 8870
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB