; COMMAND-LINE: --strings-exp --incremental
(set-logic QF_S)
(declare-const Str0 String)
(declare-const Str1 String)
(declare-const Str2 String)
(declare-const Str3 String)
(declare-const Str4 String)
(declare-const Str5 String)
(declare-const Str6 String)
(declare-const Str7 String)
(declare-const Str8 String)
(declare-const Str9 String)
(declare-const Str10 String)
(declare-const Str11 String)
(declare-const Str12 String)
(declare-const Str13 String)
(declare-const Str14 String)
(declare-const Str15 String)
(declare-const Str16 String)
(declare-const Str17 String)
(declare-const Str18 String)
(declare-const Str19 String)
(assert (str.in_re Str19(re.opt (str.to_re Str10))))
(assert (str.in_re Str9(re.opt (str.to_re Str18))))
(assert (str.in_re (str.replace Str12 "jkngjj" Str14)(re.opt (str.to_re (str.++ Str13 "spifluyxzmbznnejkmfajdisgnyfeogvtwxuclzmrlmjmmwhly" Str5 Str19 "rsjusudbyjoyfpwbpasemhhxoayzouhoaekszsvhbsmnysbcih")))))
(assert (str.in_re Str13(re.opt (str.to_re Str3))))
(push 1)
(assert (str.in_re (str.++ Str12 (str.++ Str5 Str16 Str13) (str.++ Str5 "tqckdn" "hvhftx" (str.replace Str12 "jkngjj" Str14)) "trcuij" "ovnscketrkugxyqewkvuvondgahkfzwczexnyiziwhyqlomqie")(re.opt (str.to_re Str8))))
(push 1)
(assert (str.in_re (str.++ Str13 (str.++ Str5 Str16 Str13))(re.++ (str.to_re (str.++ Str5 Str16 Str13)) (str.to_re "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs" ))))
(set-info :status sat)
(check-sat)