diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 691ecd737..d2e26334b 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2226,6 +2226,15 @@ public class Context implements AutoCloseable { return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject())); } + /** + * Extract the last index of sub-string. + */ + public final IntExpr mkLastIndexOf(Expr> s, Expr> substr) + { + checkContextMatch(s, substr); + return (IntExpr)Expr.create(this, Native.mkSeqLastIndex(nCtx(), s.getNativeObject(), substr.getNativeObject())); + } + /** * Replace the first occurrence of src by dst in s. */ diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index f612b9031..4910338f3 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -144,6 +144,8 @@ public class Sort extends AST return new SeqSort<>(ctx, obj); case Z3_RE_SORT: return new ReSort<>(ctx, obj); + case Z3_CHAR_SORT: + return new CharSort(ctx, obj); default: throw new Z3Exception("Unknown sort kind"); }