From df75792e9c43ebd456b5ccca1a44da35a3456c27 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Jun 2020 18:35:38 -0700 Subject: [PATCH] fix #4454 Signed-off-by: Nikolaj Bjorner --- src/api/java/Context.java | 10 ++++++++++ 1 file changed, 10 insertions(+) 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. */