Puzzling "operator is applied to arguments of the wrong sort" with mkConcat in Java API #7568
Unanswered
yvanlabiche
asked this question in
Q&A
Replies: 0 comments
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
-
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.
Beta Was this translation helpful? Give feedback.
All reactions