Puzzling "operator is applied to arguments of the wrong sort" with mkConcat in Java API

[yvanlabiche]

Hello,
I am using the Java API.
I am calling ctx.mkConcat(expr1, expr2), ctx being a Z3 context. expr1 and expr2 are produced by other complicated statements, which are too long to explain here.
However, I checked with calls to (Java) expr1.getClass() and (Z3) expr1.getSort() or expr1.getSort().getSortKind().
On both arguments expr1 and expr2 I get com.microsoft.z3.SeqExpr, String, and Z3_SEQ_SORT, respectively.
All this makes sense to me and, in my opinion, matches the signature of mkConcat, but I nevertheless receive message "operator is applied to arguments of the wrong sort". Why is that?
On a related note, is there a way to get an error/exception message from Z3 that is more specific than "operator is applied to arguments of the wrong sort"? I mean the message I get does not indicate what sorts are expected for instance; It does not refer to the use of mkConcat (I had to dig into the code and find that if I replace the call to mkConcat with something dummy the error disappears).
Thank you in advance.