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