diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 3987004ef..0293fc76a 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2488,12 +2488,12 @@ namespace Microsoft.Z3 /// /// Retrieve element at index. /// - public SeqExpr MkNth(SeqExpr s, Expr index) + public Expr MkNth(SeqExpr s, Expr index) { Debug.Assert(s != null); Debug.Assert(index != null); CheckContextMatch(s, index); - return new SeqExpr(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject)); + return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject)); } /// diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 31c9771b1..06fe6061a 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2051,10 +2051,10 @@ public class Context implements AutoCloseable { /** * Retrieve element at index. */ - public SeqExpr MkNth(SeqExpr s, Expr index) + public Expr MkNth(SeqExpr s, Expr index) { checkContextMatch(s, index); - return (SeqExpr) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); + return Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject())); }