(set-logic QF_S) (declare-fun var0 () String) (assert (RegexIn var0 (RegexConcat (RegexStar (RegexPlus (Str2Reg "00"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "11"))) (RegexConcat (RegexStar (RegexPlus (Str2Reg "2"))) (RegexConcat (RegexUnion (RegexUnion (Str2Reg "33") (Str2Reg "44")) (RegexUnion (Str2Reg "5") (Str2Reg "66"))) (RegexConcat (RegexStar (RegexStar (Str2Reg "7"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "8"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "99"))) (RegexConcat (RegexPlus (RegexStar (Str2Reg "aaa"))) (RegexConcat (RegexUnion (RegexPlus (Str2Reg "b")) (RegexPlus (Str2Reg "cc"))) (RegexStar (RegexPlus (Str2Reg "d")))))))))))))) (assert (<= 1 (Length var0))) (check-sat)