test/regress/regress0/strings/loop001.smt2

   1 (set-logic ALL_SUPPORTED)
   2 (set-info :status unsat)
   3
   4 (declare-fun x () String)
   5 (declare-fun y () String)
   6 (declare-fun z () String)
   7 (declare-fun w () String)
   8 (declare-fun w1 () String)
   9 (declare-fun w2 () String)
  10
  11 (assert (= (str.++ x "a") (str.++ "b" x)))
  12
  13 (check-sat)