diff --git a/src/api/java/Context.java b/src/api/java/Context.java index ef1f6bb07..3de37129e 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2048,6 +2048,16 @@ public class Context implements AutoCloseable { return (SeqExpr) Expr.create(this, Native.mkSeqAt(nCtx(), s.getNativeObject(), index.getNativeObject())); } + /** + * Retrieve element at index. + */ + public SeqExpr MkNth(SeqExpr s, Expr index) + { + checkContextMatch(s, index); + return (SeqExpr) Expr.create(this, Native.Z3_mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); + } + + /** * Extract subsequence. */