(set-logic QF_S) (declare-fun var0 () String) (assert (RegexIn var0 (RegexConcat (Str2Reg "00") (Str2Reg "111")))) (assert (<= 15 (Length var0))) (check-sat)