(set-logic QF_S)
(declare-fun var0 () String)
(declare-fun var1 () String)
(declare-fun var2 () String)
(declare-fun var3 () String)
(declare-fun var4 () String)
(declare-fun var5 () String)
(declare-fun var6 () String)
(declare-fun var7 () String)
(declare-fun var8 () String)
(declare-fun var9 () String)
(assert (= 33 (str.len var0)))
(assert (= 1 (str.len var1)))
(assert (= 49 (str.len var2)))
(assert (= 50 (str.len var3)))
(assert (= 25 (str.len var4)))
(assert (= 3 (str.len var5)))
(assert (= 77 (str.len var6)))
(assert (= 20 (str.len var7)))
(assert (= 100 (str.len var8)))
(assert (= 7 (str.len var9)))
(assert (= 84 (str.len (str.++ var6 var9))))
(check-sat)