Bugs in Z3 regard to String Theory

[Mingyu821]

1. First, I cannot appoint class of ctx.mkToRe(ctx.mkString("")) to Expr<ReSort<SeqSort<CharSort>>>. It will result in an error in ctx.mkConcat. Is there any incompatibles in appointing exact classes?
2. Second, ctx.mkOption api is not compatible when I want to use this api to perform "?" in Re expressions.

Code seen below:

public static BoolExpr addRegexOrTerms(List<String> regexList, Context ctx, Expr<SeqSort<CharSort>> var) {
        Expr<ReSort<SeqSort<CharSort>>> concat = ctx.mkToRe(ctx.mkString(""));
        Expr res;
        BoolExpr expr = ctx.mkFalse();
        for (String s : regexList) {
            for (int i = 0; i < s.length(); i++) {
                switch (s.charAt(i)) {
                    case '*':
                        res = ctx.mkFullRe(ctx.mkReSort(ctx.mkStringSort()));
                        break;
                    case '?':
                        res = ctx.mkOption(ctx.mkReSort(ctx.mkStringSort()));
                        break;
                    default:
                        res = ctx.mkToRe(ctx.mkString(String.valueOf(s.charAt(i))));
                }
                concat = ctx.mkConcat(concat, res);
            }
            expr = ctx.mkOr(expr, ctx.mkInRe(var, concat.simplify()));
        }
        return expr;
    }

[NikolajBjorner]

public static BoolExpr addRegexOrTerms(List<String> regexList, Context ctx, Expr<SeqSort<CharSort>> var) {
        ReExpr<SeqSort<CharSort>> concat = ctx.mkToRe(ctx.mkString(""));
        ReExpr<SeqSort<CharSort>> res;
        BoolExpr expr = ctx.mkFalse();
        for (String s : regexList) {
            for (int i = 0; i < s.length(); i++) {
                switch (s.charAt(i)) {
                    case '*':
                        res = ctx.mkFullRe(ctx.mkReSort(ctx.mkStringSort()));
                        break;
                    case '?':
                        res = ctx.mkOption(ctx.mkToRe(ctx.mkString(String.valueOf(s.charAt(i)))));
                        break;
                    default:
                        res = ctx.mkToRe(ctx.mkString(String.valueOf(s.charAt(i))));
                }
                concat = ctx.mkConcat(concat, res);
            }
            expr = ctx.mkOr(expr, ctx.mkInRe(var, concat.simplify()));
        }
        return expr;
    }