(set-logic QF_S)
(declare-fun var0 () String)
(assert (RegexIn var0 (RegexStar (RegexStar (Str2Reg "000")))))
(assert (not (RegexIn var0 (RegexUnion (RegexStar (Str2Reg "0")) (RegexStar (Str2Reg "1"))))))
(check-sat)