A possible bug in Java api concat Kleene Star and Re expressions

[Mingyu821]

In Java api
ctx.mkToRe(ctx.mkString("abcd")); is used to make re expressions, of which class is ReExpr<CharSort>
ctx.mkFullRe(ctx.mkReSort(ctx.mkCharSort())); is used to make a Kleene Star, of which class is ReExpr<ReSort<CharSort>>

So, this is incompatible, how to use Kleene star in re expressions?

For example, re expression like "abc*d", where "*" represents zero or more repetitions of arbitrary string values.
ctx.mkConcat(ctx.mkToRe(ctx.mkString("abc")), ctx.mkFullRe(ctx.mkReSort(ctx.mkCharSort())), ctx.mkToRe(ctx.mkString("d")); will not make sense.

[NikolajBjorner]

ctx.mkFullRe(ctx.mkCharSort()) does not work?

[Mingyu821]

ctx.mkFullRe(ctx.mkCharSort()) does not work?

Yes, it will throw an 'java.lang.ClassCastException' Exception.

The errorCode is com.microsoft.z3.Expr cannot be cast to com.microsoft.z3.ReExpr.

[Mingyu821]

Thanks for fixing this.
However, I cannot appoint class of ctx.mkToRe(ctx.mkString("")) to Expr<ReSort<SeqSort<CharSort>>>. It will result in an error in ctx.mkConcat.
So, now I cannot appoint these class explicitly. And ctx.mkOption api is not compatible when I want to use this api to perform "?" in Re expressions.